set F = f to_power g;
thus rng (f to_power g) c= NAT :: according to RELAT_1:def 19 :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f to_power g) or y in NAT )
assume y in rng (f to_power g) ; :: thesis: y in NAT
then consider x being object such that
A1: x in dom (f to_power g) and
A2: (f to_power g) . x = y by FUNCT_1:def 3;
(f to_power g) . x = (f . x) to_power (g . x) by A1, Def6;
hence y in NAT by A2, ORDINAL1:def 12; :: thesis: verum

end;