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

proof

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

end;

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