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 ;
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 ;
then (H ") . x in rng (H ") by FUNCT_1:def 3;
then A8: (H ") . x in dom G by ;
then G . ((H ") . x) in rng G by FUNCT_1:def 3;
then F . (H . ((H ") . x)) in rng G by ;
hence z in rng G by ; :: 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 ;
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 ;
then A15: F . x in rng F by ;
x = H . y by ;
hence z in rng F by ; :: 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