A,B:Type, f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))

Auto
THEN
AllHyps (h. FwdThru Thm* f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A; B; f; g)) [h])
THEN
ExRepD
THEN
AllHyps (h.FwdThru Thm* f:(AB), g:(BA). InvFuns(A; B; f; g) InvFuns(B; A; g; f) [h])

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)

2 steps

About: