let f, g be Function; :: thesis: ( rng f = rng g & f is one-to-one & g is one-to-one implies f,g are_fiberwise_equipotent )
assume that
A1: rng f = rng g and
A2: f is one-to-one and
A3: g is one-to-one ; :: thesis: f,g are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def 9 :: thesis: card (Coim f,x) = card (Coim g,x)

per cases ( x in rng f or not x in rng f ) ;

suppose x in rng f ; :: thesis: card (Coim f,x) = card (Coim g,x)

then ( card (f " {x}) = 1 & card (g " {x}) = 1 ) by A1, A2, A3, FINSEQ_4:88;
hence card (Coim f,x) = card (Coim g,x) ; :: thesis: verum

end;

suppose not x in rng f ; :: thesis: card (Coim f,x) = card (Coim g,x)

then ( card (f " {x}) = 0 & card (g " {x}) = 0 ) by A1, CARD_1:47, FUNCT_1:142;
hence card (Coim f,x) = card (Coim g,x) ; :: thesis: verum

end;

end;