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