let F, G be Function; :: thesis: ( F,G are_fiberwise_equipotent implies rng F = rng G )
assume A1: F,G are_fiberwise_equipotent ; :: thesis: rng F = rng G
thus rng F c= rng G :: according to XBOOLE_0:def 10 :: thesis: rng G c= rng F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in rng G )
assume that
A2: x in rng F and
A3: not x in rng G ; :: thesis: contradiction
A4: card (Coim (F,x)) = card (Coim (G,x)) by A1;
A5: ex y being object st
( y in dom F & F . y = x ) by A2, FUNCT_1:def 3;
Coim (G,x) = {} by A3, Lm3;
then ( x in {x} & F " {x} = {} ) by A4, CARD_1:5, CARD_1:26, TARSKI:def 1;
hence contradiction by A5, FUNCT_1:def 7; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in rng F )
assume that
A6: x in rng G and
A7: not x in rng F ; :: thesis: contradiction
A8: card (Coim (G,x)) = card (Coim (F,x)) by A1;
A9: ex y being object st
( y in dom G & G . y = x ) by A6, FUNCT_1:def 3;
Coim (F,x) = {} by A7, Lm3;
then ( x in {x} & Coim (G,x) = {} ) by A8, CARD_1:5, CARD_1:26, TARSKI:def 1;
hence contradiction by A9, FUNCT_1:def 7; :: thesis: verum