let F, G, H be Function; :: thesis: ( 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 ; :: 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, Def9
.= card (Coim H,x) by A2, Def9 ; :: thesis: verum