set b = f | J;
consider f' being FinSequence of REAL such that
A1: Sum (f | J) = Sum f' and
A2: f' = (f | J) * (canFS (support (f | J))) by UPROOTS:def 3;
rng f' c= NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f' or y in NAT )
assume y in rng f' ; :: thesis: y in NAT
hence y in NAT by A2, ORDINAL1:def 13; :: thesis: verum

end;

then reconsider f' = f' as FinSequence of NAT by FINSEQ_1:def 4;
Sum f' is Element of NAT ;
hence for b₁ being number st b₁ = Sum (f | J) holds
b₁ is natural by A1; :: thesis: verum