(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: inverse-biject 1
1. A: Type
2. B: Type
3. f: AB
4. Bij(A; B; f)
5. g: BA
6. InvFuns(A; B; f; g)
7. InvFuns(B; A; g; f)
g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g)
By: InstConcl [g]
Generated subgoal:

1 Bij(B; A; g)1 step

About:
functionuniverseandexists

(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc