let D be non empty set ; :: thesis: for F, G being Function st rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim F,d) = card (Coim G,d) ) holds
F,G are_fiberwise_equipotent
let F, G be Function; :: thesis: ( rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim F,d) = card (Coim G,d) ) implies F,G are_fiberwise_equipotent )
assume that
A1: rng F c= D and
A2: rng G c= D ; :: thesis: ( ex d being Element of D st not card (Coim F,d) = card (Coim G,d) or F,G are_fiberwise_equipotent )
assume A3: for d being Element of D holds card (Coim F,d) = card (Coim G,d) ; :: 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 ( not x in rng F or x in rng F ) ;

suppose not x in rng F ; :: thesis: card (Coim F,x) = card (Coim G,x)

then A5: Coim F,x = {} by Lm3;

now

assume A7: x in rng G ; :: thesis: contradiction
then reconsider d = x as Element of D by A2;
card (Coim G,d) = card (Coim F,d) by A3;
then G " {d},F " {d} are_equipotent by CARD_1:21;
then A10: G " {x} = {} by A5, CARD_1:46;
consider y being set such that
A11: y in dom G and
A12: G . y = x by A7, FUNCT_1:def 5;
G . y in {x} by A12, TARSKI:def 1;
hence contradiction by A10, A11, FUNCT_1:def 13; :: thesis: verum

end;

hence card (Coim F,x) = card (Coim G,x) by A5, Lm3; :: thesis: verum

end;

suppose x in rng F ; :: thesis: card (Coim F,x) = card (Coim G,x)

then reconsider d = x as Element of D by A1;
card (Coim F,d) = card (Coim G,d) by A3;
hence card (Coim F,x) = card (Coim G,x) ; :: thesis: verum

end;

end;