set cS = canFS (support b);

let n be Element of NAT ; :: thesis: ( n = Sum b iff ex f being FinSequence of NAT st

( n = Sum f & f = b * (canFS (support 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 A11, Def2; :: thesis: verum

let n be Element of NAT ; :: thesis: ( n = Sum b iff ex f being FinSequence of NAT st

( n = Sum f & f = b * (canFS (support b)) ) )

hereby :: thesis: ( ex f being FinSequence of NAT st

( n = Sum f & f = b * (canFS (support b)) ) implies n = Sum b )

given f being FinSequence of NAT such that A11:
( n = Sum f & f = b * (canFS (support b)) )
; :: thesis: n = Sum b( n = Sum f & f = b * (canFS (support b)) ) implies n = Sum b )

consider f being FinSequence of REAL such that

A5: degree b = Sum f and

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

A7: rng f c= NAT

( n = Sum f & f = b * (canFS (support b)) )

reconsider f = f as FinSequence of NAT by A7, FINSEQ_1:def 4;

take f = f; :: thesis: ( n = Sum f & f = b * (canFS (support b)) )

thus ( n = Sum f & f = b * (canFS (support b)) ) by A10, A5, A6; :: thesis: verum

end;A5: degree b = Sum f and

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

A7: rng f c= NAT

proof

assume A10:
n = degree b
; :: thesis: ex f being FinSequence of NAT st
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

A8: x in dom f and

A9: y = f . x by FUNCT_1:def 3;

f . x = b . ((canFS (support b)) . x) by A6, A8, FUNCT_1:12;

hence y in NAT by A9; :: thesis: verum

end;assume y in rng f ; :: thesis: y in NAT

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 (support b)) . x) by A6, A8, FUNCT_1:12;

hence y in NAT by A9; :: thesis: verum

( n = Sum f & f = b * (canFS (support b)) )

reconsider f = f as FinSequence of NAT by A7, FINSEQ_1:def 4;

take f = f; :: thesis: ( n = Sum f & f = b * (canFS (support b)) )

thus ( n = Sum f & f = b * (canFS (support b)) ) by A10, A5, A6; :: thesis: verum

rng f c= REAL ;

then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;

f = f ;

hence n = Sum b by A11, Def2; :: thesis: verum