rng fp c= NAT by VALUED_0:def 6;
then reconsider fp = fp as FinSequence of NAT by FINSEQ_1:def 4;
Sum fp in NAT ;
hence Sum fp is natural ; :: thesis: verum