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
A2: H is one-to-one and
A3: dom H = Y and
A4: rng H = X by 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;
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 set such that
A9: x in dom F and
A10: z = F . x by FUNCT_1:def 5;
x in rng H by A4, A9;
then x in dom (H " ) by A2, FUNCT_1:54;
then (H " ) . x in rng (H " ) by FUNCT_1:def 5;
then A14: (H " ) . x in dom G by A2, A3, A6, FUNCT_1:55;
then G . ((H " ) . x) in rng G by FUNCT_1:def 5;
then F . (H . ((H " ) . x)) in rng G by A14, FUNCT_1:22;
hence z in rng G by A2, A4, A9, A10, FUNCT_1:57; :: thesis: verum

end;

then A17: rng F c= rng G by SUBSET_1:7;
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 set such that
A20: y in dom G and
A21: z = G . y by FUNCT_1:def 5;
y in rng (H " ) by A2, A3, A6, A20, FUNCT_1:55;
then consider x being set such that
A23: x in dom (H " ) and
A24: y = (H " ) . x by FUNCT_1:def 5;
A25: x in rng H by A2, A23, FUNCT_1:55;
then A26: F . x in rng F by A5, FUNCT_1:def 5;
x = H . y by A2, A24, A25, FUNCT_1:54;
hence z in rng F by A20, A21, A26, FUNCT_1:22; :: thesis: verum

end;

then rng G c= rng F by SUBSET_1:7;
then rng F = rng G by A17, XBOOLE_0:def 10;
hence ex G being Function of Y,Z st rng F = rng G ; :: thesis: verum