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 and
A2: rng H = dom G and
A3: H is one-to-one and
A4: F = G * H by Th77;
let X be set ; :: thesis:
set t = H | (F " X);
A5: H | (F " X) is one-to-one by A3, FUNCT_1:52;
A6: dom (H | (F " X)) = F " X by A1, RELAT_1:62, RELAT_1:132;
rng (H | (F " X)) = G " X

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

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng (H | (F " X)) ; :: thesis:
then consider y being object such that
A7: y in dom (H | (F " X)) and
A8: (H | (F " X)) . y = z by FUNCT_1:def 3;
A9: F . y in X by A6, A7, FUNCT_1:def 7;
A10: z = H . y by A7, A8, FUNCT_1:47;
dom (H | (F " X)) = (dom H) /\ (F " X) by RELAT_1:61;
then A11: y in dom H by A7, XBOOLE_0:def 4;
then A12: z in dom G by A2, A10, FUNCT_1:def 3;
G . z in X by A4, A9, A10, A11, FUNCT_1:13;
hence z in G " X by A12, FUNCT_1:def 7; :: thesis:

end;

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: z in G " X ; :: thesis:
then A14: z in dom G by FUNCT_1:def 7;
A15: G . z in X by A13, FUNCT_1:def 7;
consider y being object such that
A16: y in dom H and
A17: H . y = z by A2, A14, FUNCT_1:def 3;
F . y in X by A4, A15, A16, A17, FUNCT_1:13;
then A18: y in dom (H | (F " X)) by A1, A6, A16, FUNCT_1:def 7;
then (H | (F " X)) . y in rng (H | (F " X)) by FUNCT_1:def 3;
hence z in rng (H | (F " X)) by A17, A18, FUNCT_1:47; :: thesis:

end;

hence card (F " X) = card (G " X) by CARD_1:5, A5, A6, WELLORD2:def 4; :: thesis:

end;

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