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 object ; :: according to CLASSES1:def 10 :: 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 A4: Coim (F,x) = {} by Lm3;

now :: thesis: not x in rng G

assume A5: 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 A6: G " {x} = {} by A4, CARD_1:5, CARD_1:26;
consider y being object such that
A7: y in dom G and
A8: G . y = x by A5, FUNCT_1:def 3;
G . y in {x} by A8, TARSKI:def 1;
hence contradiction by A6, A7, FUNCT_1:def 7; :: thesis: verum

end;

hence card (Coim (F,x)) = card (Coim (G,x)) by A4, 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;