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 A1: ( rng F c= D & 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 A2: 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 A3: Coim F,x = {} by Lm1;

now

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

end;

hence card (Coim F,x) = card (Coim G,x) by A3, Lm1; :: 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 A2;
hence card (Coim F,x) = card (Coim G,x) ; :: thesis: verum

end;

end;