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

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