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;