let F, G be Function; :: thesis:
thus ( F,G are_fiberwise_equipotent implies for X being set holds card (F " X) = card (G " X) ) :: thesis:

assume F,G are_fiberwise_equipotent ; :: thesis:
then consider H being Function such that
A1: ( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) by Th3;
let X be set ; :: thesis:
set t = H | (F " X);
A2: H | (F " X) is one-to-one by A1, FUNCT_1:84;
A3: dom (H | (F " X)) = F " X by A1, RELAT_1:91, RELAT_1:167;
rng (H | (F " X)) = G " X

thus rng (H | (F " X)) c= G " X :: according to XBOOLE_0:def 10 :: thesis:

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng (H | (F " X)) ; :: thesis:
then consider y being set such that
A4: ( y in dom (H | (F " X)) & (H | (F " X)) . y = z ) by FUNCT_1:def 5;
A5: F . y in X by A3, A4, FUNCT_1:def 13;
A6: z = H . y by A4, FUNCT_1:70;
dom (H | (F " X)) = (dom H) /\ (F " X) by RELAT_1:90;
then A7: y in dom H by A4, XBOOLE_0:def 4;
then A8: z in dom G by A1, A6, FUNCT_1:def 5;
G . z in X by A1, A5, A6, A7, FUNCT_1:23;
hence z in G " X by A8, FUNCT_1:def 13; :: thesis:

end;

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in G " X ; :: thesis:
then A9: ( z in dom G & G . z in X ) by FUNCT_1:def 13;
then consider y being set such that
A10: ( y in dom H & H . y = z ) by A1, FUNCT_1:def 5;
F . y in X by A1, A9, A10, FUNCT_1:23;
then A11: y in dom (H | (F " X)) by A1, A3, A10, FUNCT_1:def 13;
then (H | (F " X)) . y in rng (H | (F " X)) by FUNCT_1:def 5;
hence z in rng (H | (F " X)) by A10, A11, FUNCT_1:70; :: thesis:

end;

then F " X,G " X are_equipotent by A2, A3, WELLORD2:def 4;
hence card (F " X) = card (G " X) by CARD_1:21; :: thesis:

end;

assume for X being set holds card (F " X) = card (G " X) ; :: thesis:
hence for x being set holds card (Coim F,x) = card (Coim G,x) ; :: according to CLASSES1:def 9 :: thesis: