f:(A
B), R:(BBProp).
Bij(A; B; f) 
(EquivRel x,y:B. x R y)
(
F:((x,y:A//(x R_f y))(x,y:B//(x R y))).
Bij(x,y:A//(x R_f y); x,y:B//(x R y); F))
quotient_1_1_corr
Thm* f:(AB), R:(BBProp).
Bij(A; B; f)
(EquivRel x,y:B. x R y)
(F:((x,y:A//(x R_f y))(x,y:B//(x R y))).
Bij(x,y:A//(x R_f y); x,y:B//(x R y); F))
quotient_1_1_corr
In prior sections: fun 1