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 A4: x in rng f ; :: thesis: card (Coim f,x) = card (Coim g,x)

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

end;

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

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

end;

end;