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

proof

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;

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; :: 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;

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 ; :: thesis: verum