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
X,Y are_equipotent
; ex G being Function of Y,Z st rng F = rng G
then consider H being Function such that
A1:
H is one-to-one
and
A2:
dom H = Y
and
A3:
rng H = X
by WELLORD2:def 4;
reconsider H = H as Function of Y,X by A2, A3, FUNCT_2:2;
reconsider G = F * H as Function of Y,Z ;
A4:
dom F = X
by FUNCT_2:def 1;
A5:
dom G = Y
by FUNCT_2:def 1;
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
z in rng F
;
z in rng G
then consider x being
object such that A6:
x in dom F
and A7:
z = F . x
by FUNCT_1:def 3;
x in rng H
by A3, A6;
then
x in dom (H ")
by A1, FUNCT_1:32;
then
(H ") . x in rng (H ")
by FUNCT_1:def 3;
then A8:
(H ") . x in dom G
by A1, A2, A5, FUNCT_1:33;
then
G . ((H ") . x) in rng G
by FUNCT_1:def 3;
then
F . (H . ((H ") . x)) in rng G
by A8, FUNCT_1:12;
hence
z in rng G
by A1, A3, A6, A7, FUNCT_1:35;
verum
end;
then A9:
rng F c= rng G
;
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
z in rng G
;
z in rng F
then consider y being
object such that A10:
y in dom G
and A11:
z = G . y
by FUNCT_1:def 3;
y in rng (H ")
by A1, A2, A5, A10, FUNCT_1:33;
then consider x being
object such that A12:
x in dom (H ")
and A13:
y = (H ") . x
by FUNCT_1:def 3;
A14:
x in rng H
by A1, A12, FUNCT_1:33;
then A15:
F . x in rng F
by A4, FUNCT_1:def 3;
x = H . y
by A1, A13, A14, FUNCT_1:32;
hence
z in rng F
by A10, A11, A15, FUNCT_1:12;
verum
end;
then
rng G c= rng F
;
then
rng F = rng G
by A9;
hence
ex G being Function of Y,Z st rng F = rng G
; verum