let F, G be Function; ( F,G are_fiberwise_equipotent iff for X being set holds card (F " X) = card (G " X) )
thus
( F,G are_fiberwise_equipotent implies for X being set holds card (F " X) = card (G " X) )
( ( for X being set holds card (F " X) = card (G " X) ) implies F,G are_fiberwise_equipotent )proof
assume A1:
F,
G are_fiberwise_equipotent
;
for X being set holds card (F " X) = card (G " X)
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 A1, Th85;
let X be
set ;
card (F " X) = card (G " X)
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;
A8:
rng (H | (F " X)) = G " X
proof
thus
rng (H | (F " X)) c= G " X
XBOOLE_0:def 10 G " X c= rng (H | (F " X))proof
let z be
set ;
TARSKI:def 3 ( not z in rng (H | (F " X)) or z in G " X )
assume A9:
z in rng (H | (F " X))
;
z in G " X
consider y being
set such that A10:
y in dom (H | (F " X))
and A11:
(H | (F " X)) . y = z
by A9, 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;
A14:
dom (H | (F " X)) = (dom H) /\ (F " X)
by RELAT_1:90;
A15:
y in dom H
by A10, A14, XBOOLE_0:def 4;
A16:
z in dom G
by A3, A13, A15, FUNCT_1:def 5;
A17:
G . z in X
by A5, A12, A13, A15, FUNCT_1:23;
thus
z in G " X
by A16, A17, FUNCT_1:def 13;
verum
end;
let z be
set ;
TARSKI:def 3 ( not z in G " X or z in rng (H | (F " X)) )
assume A18:
z in G " X
;
z in rng (H | (F " X))
A19:
z in dom G
by A18, 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;
A23:
F . y in X
by A5, A20, A21, A22, FUNCT_1:23;
A24:
y in dom (H | (F " X))
by A2, A7, A21, A23, FUNCT_1:def 13;
A25:
(H | (F " X)) . y in rng (H | (F " X))
by A24, FUNCT_1:def 5;
thus
z in rng (H | (F " X))
by A22, A24, A25, FUNCT_1:70;
verum
end;
A26:
F " X,
G " X are_equipotent
by A6, A7, A8, WELLORD2:def 4;
thus
card (F " X) = card (G " X)
by A26, CARD_1:21;
verum
end;
assume A27:
for X being set holds card (F " X) = card (G " X)
; F,G are_fiberwise_equipotent
thus
for x being set holds card (Coim F,x) = card (Coim G,x)
by A27; CLASSES1:def 9 verum