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)) ) )
hereby :: thesis: ( ex f being FinSequence of NAT st
( 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
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
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 A10: n = degree b ; :: thesis: ex f being FinSequence of NAT st
( 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;
given f being FinSequence of NAT such that A11: ( n = Sum f & f = b * (canFS (support b)) ) ; :: 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 A11, Def2; :: thesis: verum