We are students at the computer science department of the university of Eindhoven in The Netherlands. Because of a schoolproject we are trying to prove serveral lemma's in theorem prover PVS. On the internet we found some published work of in PVS, and therefor we hope you would like to help us.
We use PVS for the following prove:
Let V be a set, A and B a subset of V, f:A->B and g:B->A.
If f and g are both surjective then there is a bijection h:A->B.
Hopefully you could make some recommendations for us.
Rob Urlings and Loek Simons