set F = f to_power g;
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 (f to_power g) or not r <= 0 )
assume r in rng (f to_power g) ; :: thesis: not r <= 0
then consider x being object such that
A1: x in dom (f to_power g) and
A2: (f to_power g) . x = r by FUNCT_1:def 3;
dom (f to_power g) = (dom f) /\ (dom g) by Def6;
then A3: ( f . x in rng f & g . x in rng g ) by A1, FUNCT_1:def 3;
(f to_power g) . x = (f . x) to_power (g . x) by A1, Def6;
hence r > 0 by A2, A3; :: thesis: verum