reconsider FR = F_Real as Field ;
reconsider P = p as Polynomial of O,FR ;
set S = SgmX ((),());
consider f being sequence of FR such that
A1: ( Sum (P * (SgmX ((),()))) = f . (len (P * (SgmX ((),())))) & f . 0 = 0. FR ) and
A2: for j being Nat
for v being Element of FR st j < len (P * (SgmX ((),()))) & v = (P * (SgmX ((),()))) . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S1[ Nat] means ( O <= len (P * (SgmX ((),()))) implies f . O is natural );
A3: S1[ 0 ] by A1;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
assume A5: S1[n] ; :: thesis: S1[n + 1]
assume A6: n + 1 <= len (P * (SgmX ((),()))) ; :: thesis: f . (n + 1) is natural
then A7: n + 1 in dom (P * (SgmX ((),()))) by ;
A8: (P * (SgmX ((),()))) . (n + 1) = (P * (SgmX ((),()))) /. (n + 1) by ;
reconsider psn1 = (P * (SgmX ((),()))) /. (n + 1) as Nat by A8;
reconsider fn = f . n as Nat by ;
(f . n) + ((P * (SgmX ((),()))) /. (n + 1)) = fn + psn1 by BINOP_2:def 9;
hence f . (n + 1) is natural by ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
hence sum_of_coefficients p is natural by A1; :: thesis: verum