let D be non empty set ; :: thesis:
let F, G be Function; :: thesis:
assume that
A1: rng F c= D and
A2: rng G c= D ; :: thesis:
assume A3: for d being Element of D holds card (Coim (F,d)) = card (Coim (G,d)) ; :: thesis:
let x be object ; :: according to CLASSES1:def 10 :: thesis:

per cases ;

suppose not x in rng F ; :: thesis:

then A4: Coim (F,x) = {} by Lm3;

now :: thesis:

assume A5: x in rng G ; :: thesis:
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:

end;

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

end;

suppose x in rng F ; :: thesis:

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:

end;

end;