now :: thesis: for x being object st x in dom (n |^ f) holds
(n |^ f) . x is natural

let x be object ; :: thesis: ( x in dom (n |^ f) implies (n |^ f) . x is natural )
assume x in dom (n |^ f) ; :: thesis: (n |^ f) . x is natural
then x in dom f by Def4;
then (n |^ f) . x = n to_power (f . x) by Def4;
hence (n |^ f) . x is natural ; :: thesis: verum

end;

hence n |^ f is natural-valued by VALUED_0:def 12; :: thesis: verum