consider f being FinSequence of REAL such that
A1: degree b = Sum f and
A2: f = b * (canFS (support b)) by Def2;
rng f c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being object such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 3;
f . x = b . ((canFS (support b)) . x) by A2, A3, FUNCT_1:12;
hence y in NAT by A4; :: thesis: verum

end;

then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
Sum f is Element of NAT ;
hence Sum b is Element of NAT by A1; :: thesis: verum