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 & dom H = Y & rng H = X ) by WELLORD2:def 4;
reconsider H = H as Function of Y,X by A1, FUNCT_2:4;
reconsider G = F * H as Function of Y,Z ;
A2: ( dom F = X & 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
A3: ( x in dom F & z = F . x ) by FUNCT_1:def 5;
x in rng H by A1, A3;
then x in dom (H " ) by A1, FUNCT_1:54;
then (H " ) . x in rng (H " ) by FUNCT_1:def 5;
then A4: (H " ) . x in dom G by A1, A2, FUNCT_1:55;
then G . ((H " ) . x) in rng G by FUNCT_1:def 5;
then F . (H . ((H " ) . x)) in rng G by A4, FUNCT_1:22;
hence z in rng G by A1, A3, FUNCT_1:57; :: thesis: verum

end;

then A5: 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
A6: ( y in dom G & z = G . y ) by FUNCT_1:def 5;
y in rng (H " ) by A1, A2, A6, FUNCT_1:55;
then consider x being set such that
A7: ( x in dom (H " ) & y = (H " ) . x ) by FUNCT_1:def 5;
A8: x in rng H by A1, A7, FUNCT_1:55;
then A9: F . x in rng F by A2, FUNCT_1:def 5;
x = H . y by A1, A7, A8, FUNCT_1:54;
hence z in rng F by A6, A9, FUNCT_1:22; :: thesis: verum

end;

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