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
A2: dom H = dom F and
A3: rng H = dom G and
A4: H is one-to-one and
A5: F = G * H by Th85;
let X be set ; :: thesis:
set t = H | (F " X);
A6: H | (F " X) is one-to-one by A4, FUNCT_1:84;
A7: dom (H | (F " X)) = F " X by A2, 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
A10: y in dom (H | (F " X)) and
A11: (H | (F " X)) . y = z by FUNCT_1:def 5;
A12: F . y in X by A7, A10, FUNCT_1:def 13;
A13: z = H . y by A10, A11, FUNCT_1:70;
dom (H | (F " X)) = (dom H) /\ (F " X) by RELAT_1:90;
then A15: y in dom H by A10, XBOOLE_0:def 4;
then A16: z in dom G by A3, A13, FUNCT_1:def 5;
G . z in X by A5, A12, A13, A15, FUNCT_1:23;
hence z in G " X by A16, FUNCT_1:def 13; :: thesis:

end;

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A18: z in G " X ; :: thesis:
then A19: z in dom G by FUNCT_1:def 13;
A20: G . z in X by A18, FUNCT_1:def 13;
consider y being set such that
A21: y in dom H and
A22: H . y = z by A3, A19, FUNCT_1:def 5;
F . y in X by A5, A20, A21, A22, FUNCT_1:23;
then A24: y in dom (H | (F " X)) by A2, A7, A21, 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 A22, A24, FUNCT_1:70; :: thesis:

end;

then F " X,G " X are_equipotent by A6, A7, 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: