is mentioned by

Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))	[inverse-biject]
Thm* f:(AB), g:(BC). Bij(A; B; f) Bij(B; C; g) Bij(A; C; g o f)	[compose-biject]
Thm* Bij(T; T; Id)	[identity-biject]

In prior sections: fun 1 mb nat mb list 1 mb list 2

Try larger context: Graphs