let F, G, H be Function; :: thesis: ( F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent implies G,H are_fiberwise_equipotent )
assume A1: ( F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent ) ; :: thesis: G,H are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def 9 :: thesis: card (Coim G,x) = card (Coim H,x)
thus card (Coim G,x) = card (Coim F,x) by A1, Def1
.= card (Coim H,x) by A1, Def1 ; :: thesis: verum