set cS = canFS ();
let n be Element of NAT ; :: thesis: ( n = Sum b iff ex f being FinSequence of NAT st
( n = Sum f & f = b * (canFS ()) ) )

hereby :: thesis: ( ex f being FinSequence of NAT st
( n = Sum f & f = b * (canFS ()) ) implies n = Sum b )
consider f being FinSequence of REAL such that
A5: degree b = Sum f and
A6: f = b * (canFS ()) by Def2;
A7: 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:
then consider x being object such that
A8: x in dom f and
A9: y = f . x by FUNCT_1:def 3;
f . x = b . ((canFS ()) . x) by ;
hence y in NAT by A9; :: thesis: verum
end;
assume A10: n = degree b ; :: thesis: ex f being FinSequence of NAT st
( n = Sum f & f = b * (canFS ()) )

reconsider f = f as FinSequence of NAT by ;
take f = f; :: thesis: ( n = Sum f & f = b * (canFS ()) )
thus ( n = Sum f & f = b * (canFS ()) ) by A10, A5, A6; :: thesis: verum
end;
given f being FinSequence of NAT such that A11: ( n = Sum f & f = b * (canFS ()) ) ; :: thesis: n = Sum b
rng f c= REAL ;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
f = f ;
hence n = Sum b by ; :: thesis: verum