rng (f ^\ n) c= rng f
by NAT_1:55;

then for r being Real st r in rng (f ^\ n) holds

0 <= r by PARTFUN3:def 4;

hence f ^\ n is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum

then for r being Real st r in rng (f ^\ n) holds

0 <= r by PARTFUN3:def 4;

hence f ^\ n is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum