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