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 S1[ Nat] means ( O <= len y implies f . O is integer );
A5:
S1[ 0 ]
by A3;
A6:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A7:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
assume A8:
n + 1
<= len y
;
f . (n + 1) is integer
A9:
dom y = dom (SgmX ((BagOrder O),(Support P)))
by A1, FINSEQ_3:29;
set I =
(p * (SgmX ((BagOrder O),(Support P)))) /. (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:
(
(p * (SgmX ((BagOrder O),(Support P)))) /. (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 =
(p * (SgmX ((BagOrder O),(Support P)))) /. (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;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A5, A6);
hence
eval (p,x) is integer
by A1, A3; verum