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
F,
G are_fiberwise_equipotent
;
for X being set holds card (F " X) = card (G " X)
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 ;
card (F " X) = card (G " X)
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
proof
thus
rng (H | (F " X)) c= G " X
XBOOLE_0:def 10 G " X c= rng (H | (F " X))proof
let z be
object ;
TARSKI:def 3 ( not z in rng (H | (F " X)) or z in G " X )
assume
z in rng (H | (F " X))
;
z in G " X
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;
verum
end;
let z be
object ;
TARSKI:def 3 ( not z in G " X or z in rng (H | (F " X)) )
assume A13:
z in G " X
;
z in rng (H | (F " X))
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;
verum
end;
hence
card (F " X) = card (G " X)
by CARD_1:5, A5, A6, WELLORD2:def 4;
verum
end;
assume
for X being set holds card (F " X) = card (G " X)
; F,G are_fiberwise_equipotent
hence
for x being object holds card (Coim (F,x)) = card (Coim (G,x))
; CLASSES1:def 10 verum