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

let x be object ; :: thesis: ( x in dom (Sum f) implies (Sum f) . x is natural )
reconsider xx = x as set by TARSKI:1;
assume x in dom (Sum f) ; :: thesis: (Sum f) . x is natural
A1: (Sum f) . x = Sum (f . xx) by Def8;
rng (f . xx) c= NAT by VALUED_0:def 6;
then reconsider fx = f . x as FinSequence of NAT by FINSEQ_1:def 4;
Sum fx is Nat ;
hence (Sum f) . x is natural by A1; :: thesis: verum

end;

hence Sum f is natural-valued by VALUED_0:def 12; :: thesis: verum