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, Def1;
then A4: Coim F,x, Coim G,x are_equipotent by CARD_1:21;
consider y being set such that
A5: ( y in dom F & F . y = x ) by A2, FUNCT_1:def 5;
A6: x in {x} by TARSKI:def 1;
Coim G,x = {} by A3, Lm1;
then F " {x} = {} by A4, CARD_1:46;
hence contradiction by A5, 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
A7: x in rng G and
A8: not x in rng F ; :: thesis: contradiction
card (Coim G,x) = card (Coim F,x) by A1, Def1;
then A9: G " {x},F " {x} are_equipotent by CARD_1:21;
consider y being set such that
A10: ( y in dom G & G . y = x ) by A7, FUNCT_1:def 5;
A11: x in {x} by TARSKI:def 1;
Coim F,x = {} by A8, Lm1;
then Coim G,x = {} by A9, CARD_1:46;
hence contradiction by A10, A11, FUNCT_1:def 13; :: thesis: verum