set F = f to_power g;
thus rng (f to_power g) c= REAL :: 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 REAL )
assume y in rng (f to_power g) ; :: thesis: y in REAL
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 REAL by A2, XREAL_0:def 1; :: thesis: verum

end;