let F, G, H be Function; ( F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent implies G,H are_fiberwise_equipotent )
assume that
A1:
F,G are_fiberwise_equipotent
and
A2:
F,H are_fiberwise_equipotent
; G,H are_fiberwise_equipotent
let x be object ; CLASSES1:def 10 card (Coim (G,x)) = card (Coim (H,x))
thus card (Coim (G,x)) =
card (Coim (F,x))
by A1
.=
card (Coim (H,x))
by A2
; verum