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 object ; :: according to CLASSES1:def 10 :: 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 (Coim (f,x)) = 1 by A2, FINSEQ_4:73;
hence card (Coim (f,x)) = card (Coim (g,x)) by A1, A3, A4, FINSEQ_4:73; :: 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:27, FUNCT_1:72;
hence card (Coim (f,x)) = card (Coim (g,x)) by A1, A5, CARD_1:27, FUNCT_1:72; :: thesis: verum
end;
end;