reconsider FR = F_Real as non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
reconsider X = x as Function of O,FR ;
reconsider P = p as Polynomial of O,FR ;
set S = SgmX ((BagOrder O),(Support P));
consider y being FinSequence of the carrier of F_Real such that
A1: ( len y = len (SgmX ((BagOrder O),(Support P))) & eval (p,x) = Sum y ) and
A2: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((P * (SgmX ((BagOrder O),(Support P)))) /. i) * (eval (((SgmX ((BagOrder O),(Support P))) /. i),X)) by POLYNOM2:def 4;
consider f being sequence of F_Real such that
A3: ( Sum y = f . (len y) & f . 0 = 0. F_Real ) and
A4: for j being Nat
for v being Element of F_Real st j < len y & v = y . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S₁[ Nat] means ( O <= len y implies f . O is integer );
A5: S₁[ 0 ] by A3;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A8: n + 1 <= len y ; :: thesis: f . (n + 1) is integer
A9: dom y = dom (SgmX ((BagOrder O),(Support P))) by A1, FINSEQ_3:29;
reconsider A = p * (SgmX ((BagOrder O),(Support P))) as INT -valued FinSequence of the carrier of F_Real ;
set I = A /. (n + 1);
BagOrder O linearly_orders Support P by POLYNOM2:18;
then A10: rng (SgmX ((BagOrder O),(Support P))) = Support P by PRE_POLY:def 2;
dom p = Bags O by FUNCT_2:def 1;
then A11: dom (P * (SgmX ((BagOrder O),(Support P)))) = dom (SgmX ((BagOrder O),(Support P))) by A10, RELAT_1:27;
A12: n + 1 in dom y by A8, NAT_1:11, FINSEQ_3:25;
then A13: ( A /. (n + 1) = (p * (SgmX ((BagOrder O),(Support P)))) . (n + 1) & (p * (SgmX ((BagOrder O),(Support P)))) . (n + 1) = (P * (SgmX ((BagOrder O),(Support P)))) /. (n + 1) ) by A11, A9, PARTFUN1:def 6;
then reconsider PP = A /. (n + 1) as Element of F_Real ;
A14: y /. (n + 1) = PP * (eval (((SgmX ((BagOrder O),(Support P))) /. (n + 1)),x)) by A13, A2, A8, NAT_1:11;
y . (n + 1) = y /. (n + 1) by A12, PARTFUN1:def 6;
then f . (n + 1) = (f . n) + (y /. (n + 1)) by A4, A8, NAT_1:13;
hence f . (n + 1) is integer by A14, A7, A8, NAT_1:13; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
hence eval (p,x) is integer by A1, A3; :: thesis: verum