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₁[ Nat] means ( O <= len (P * (SgmX ((BagOrder O),(Support P)))) implies f . O is natural );
A3: S₁[ 0 ] by A1;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume A5: S₁[n] ; :: thesis: S₁[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;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence sum_of_coefficients p is natural by A1; :: thesis: verum