reconsider FR = F_Real as Field ;

reconsider P = p as Polynomial of O,FR ;

set S = SgmX ((BagOrder O),(Support P));

consider f being sequence of FR such that

A1: ( Sum (P * (SgmX ((BagOrder O),(Support P)))) = f . (len (P * (SgmX ((BagOrder O),(Support P))))) & f . 0 = 0. FR ) and

A2: for j being Nat

for v being Element of FR st j < len (P * (SgmX ((BagOrder O),(Support P)))) & v = (P * (SgmX ((BagOrder O),(Support P)))) . (j + 1) holds

f . (j + 1) = (f . j) + v by RLVECT_1:def 12;

defpred S_{1}[ Nat] means ( O <= len (P * (SgmX ((BagOrder O),(Support P)))) implies f . O is natural );

A3: S_{1}[ 0 ]
by A1;

A4: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A3, A4);

hence sum_of_coefficients p is natural by A1; :: thesis: verum

reconsider P = p as Polynomial of O,FR ;

set S = SgmX ((BagOrder O),(Support P));

consider f being sequence of FR such that

A1: ( Sum (P * (SgmX ((BagOrder O),(Support P)))) = f . (len (P * (SgmX ((BagOrder O),(Support P))))) & f . 0 = 0. FR ) and

A2: for j being Nat

for v being Element of FR st j < len (P * (SgmX ((BagOrder O),(Support P)))) & v = (P * (SgmX ((BagOrder O),(Support P)))) . (j + 1) holds

f . (j + 1) = (f . j) + v by RLVECT_1:def 12;

defpred S

A3: S

A4: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set n1 = n + 1;

assume A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

assume A6: n + 1 <= len (P * (SgmX ((BagOrder O),(Support P)))) ; :: thesis: f . (n + 1) is natural

then A7: n + 1 in dom (P * (SgmX ((BagOrder O),(Support P)))) by NAT_1:11, FINSEQ_3:25;

A8: (P * (SgmX ((BagOrder O),(Support P)))) . (n + 1) = (P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1) by A7, PARTFUN1:def 6;

reconsider psn1 = (P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1) as Nat by A8;

reconsider fn = f . n as Nat by A5, A6, NAT_1:13;

(f . n) + ((P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1)) = fn + psn1 by BINOP_2:def 9;

hence f . (n + 1) is natural by A8, A2, A6, NAT_1:13; :: thesis: verum

end;set n1 = n + 1;

assume A5: S

assume A6: n + 1 <= len (P * (SgmX ((BagOrder O),(Support P)))) ; :: thesis: f . (n + 1) is natural

then A7: n + 1 in dom (P * (SgmX ((BagOrder O),(Support P)))) by NAT_1:11, FINSEQ_3:25;

A8: (P * (SgmX ((BagOrder O),(Support P)))) . (n + 1) = (P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1) by A7, PARTFUN1:def 6;

reconsider psn1 = (P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1) as Nat by A8;

reconsider fn = f . n as Nat by A5, A6, NAT_1:13;

(f . n) + ((P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1)) = fn + psn1 by BINOP_2:def 9;

hence f . (n + 1) is natural by A8, A2, A6, NAT_1:13; :: thesis: verum

hence sum_of_coefficients p is natural by A1; :: thesis: verum