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 S1[ Nat] means ( O <= len (P * (SgmX ((BagOrder O),(Support P)))) 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;
( S1[n] implies S1[n + 1] )
set n1 =
n + 1;
assume A5:
S1[
n]
;
S1[n + 1]
assume A6:
n + 1
<= len (P * (SgmX ((BagOrder O),(Support P))))
;
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;
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; verum