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 set ; :: 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
card (Coim F,x) = card (Coim G,x) by A1, Def9;
then A5: Coim F,x, Coim G,x are_equipotent by CARD_1:21;
A6: ex y being set st
( y in dom F & F . y = x ) by A2, FUNCT_1:def 5;
Coim G,x = {} by A3, Lm3;
then ( x in {x} & F " {x} = {} ) by A5, CARD_1:46, TARSKI:def 1;
hence contradiction by A6, FUNCT_1:def 13; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in rng F )
assume that
A9: x in rng G and
A10: not x in rng F ; :: thesis: contradiction
card (Coim G,x) = card (Coim F,x) by A1, Def9;
then A12: G " {x},F " {x} are_equipotent by CARD_1:21;
A13: ex y being set st
( y in dom G & G . y = x ) by A9, FUNCT_1:def 5;
Coim F,x = {} by A10, Lm3;
then ( x in {x} & Coim G,x = {} ) by A12, CARD_1:46, TARSKI:def 1;
hence contradiction by A13, FUNCT_1:def 13; :: thesis: verum