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

Sum f is Element of NAT ;

hence Sum b is Element of NAT by A1; :: thesis: verum

A1: degree b = Sum f and

A2: f = b * (canFS (support b)) by Def2;

rng f c= NAT

proof

then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
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;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

Sum f is Element of NAT ;

hence Sum b is Element of NAT by A1; :: thesis: verum