let X, Y, Z be non empty set ; :: thesis: 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; :: thesis: ( X,Y are_equipotent implies ex G being Function of Y,Z st rng F = rng G )

assume X,Y are_equipotent ; :: thesis: 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

for z being Element of Z st z in rng G holds

z in rng F

then rng F = rng G by A9;

hence ex G being Function of Y,Z st rng F = rng G ; :: thesis: verum

ex G being Function of Y,Z st rng F = rng G

let F be Function of X,Z; :: thesis: ( X,Y are_equipotent implies ex G being Function of Y,Z st rng F = rng G )

assume X,Y are_equipotent ; :: thesis: 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

then A9:
rng F c= rng G
;
let z be Element of Z; :: thesis: ( z in rng F implies z in rng G )

assume z in rng F ; :: thesis: 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; :: thesis: verum

end;assume z in rng F ; :: thesis: 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; :: thesis: verum

for z being Element of Z st z in rng G holds

z in rng F

proof

then
rng G c= rng F
;
let z be Element of Z; :: thesis: ( z in rng G implies z in rng F )

assume z in rng G ; :: thesis: 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; :: thesis: verum

end;assume z in rng G ; :: thesis: 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; :: thesis: verum

then rng F = rng G by A9;

hence ex G being Function of Y,Z st rng F = rng G ; :: thesis: verum