let X, Y, Z be non empty set ; for F being Function of X,Z st X,Y are_equipotent holds
ex G being Function of Y,Z st rng F = rng G
let F be Function of X,Z; ( X,Y are_equipotent implies ex G being Function of Y,Z st rng F = rng G )
assume A1:
X,Y are_equipotent
; ex G being Function of Y,Z st rng F = rng G
consider H being Function such that
A2:
H is one-to-one
and
A3:
dom H = Y
and
A4:
rng H = X
by A1, WELLORD2:def 4;
reconsider H = H as Function of Y,X by A3, A4, FUNCT_2:4;
reconsider G = F * H as Function of Y,Z ;
A5:
dom F = X
by FUNCT_2:def 1;
A6:
dom G = Y
by FUNCT_2:def 1;
A7:
for z being Element of Z st z in rng F holds
z in rng G
proof
let z be
Element of
Z;
( z in rng F implies z in rng G )
assume A8:
z in rng F
;
z in rng G
consider x being
set such that A9:
x in dom F
and A10:
z = F . x
by A8, FUNCT_1:def 5;
A11:
x in rng H
by A4, A9;
A12:
x in dom (H " )
by A2, A11, FUNCT_1:54;
A13:
(H " ) . x in rng (H " )
by A12, FUNCT_1:def 5;
A14:
(H " ) . x in dom G
by A2, A3, A6, A13, FUNCT_1:55;
A15:
G . ((H " ) . x) in rng G
by A14, FUNCT_1:def 5;
A16:
F . (H . ((H " ) . x)) in rng G
by A14, A15, FUNCT_1:22;
thus
z in rng G
by A2, A4, A9, A10, A16, FUNCT_1:57;
verum
end;
A17:
rng F c= rng G
by A7, SUBSET_1:7;
A18:
for z being Element of Z st z in rng G holds
z in rng F
proof
let z be
Element of
Z;
( z in rng G implies z in rng F )
assume A19:
z in rng G
;
z in rng F
consider y being
set such that A20:
y in dom G
and A21:
z = G . y
by A19, FUNCT_1:def 5;
A22:
y in rng (H " )
by A2, A3, A6, A20, FUNCT_1:55;
consider x being
set such that A23:
x in dom (H " )
and A24:
y = (H " ) . x
by A22, FUNCT_1:def 5;
A25:
x in rng H
by A2, A23, FUNCT_1:55;
A26:
F . x in rng F
by A5, A25, FUNCT_1:def 5;
A27:
x = H . y
by A2, A24, A25, FUNCT_1:54;
thus
z in rng F
by A20, A21, A26, A27, FUNCT_1:22;
verum
end;
A28:
rng G c= rng F
by A18, SUBSET_1:7;
A29:
rng F = rng G
by A17, A28, XBOOLE_0:def 10;
thus
ex G being Function of Y,Z st rng F = rng G
by A29; verum