set b = f | J;
consider f9 being FinSequence of REAL such that
A1: Sum (f | J) = Sum f9 and
A2: f9 = (f | J) * (canFS (support (f | J))) by UPROOTS:def 3;
rng f9 c= NAT by A2, ORDINAL1:def 12;
then reconsider f9 = f9 as FinSequence of NAT by FINSEQ_1:def 4;
Sum f9 is Element of NAT ;
hence Sum (f | J) is natural by A1; :: thesis: verum