set SGM = SgmX ((BagOrder O),(Support p));
set PR = Polynom-Ring (O,F_Real);
consider S being FinSequence of (Polynom-Ring (O,F_Real)) such that
A1: ( Subst (p,x,s) = Sum S & len (SgmX ((BagOrder O),(Support p))) = len S ) and
A2: for i being Nat st i in dom S holds
S . i = (p . ((SgmX ((BagOrder O),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder O),(Support p))) /. i),x,s)) by Def4;
defpred S₁[ Nat] means for w being Polynomial of O,F_Real st O <= len S & w = Sum (S | O) holds
w is INT -valued ;
A3: S₁[ 0 ]

proof

reconsider Z = 0 as Nat ;
let w be Polynomial of O,F_Real; :: thesis: ( 0 <= len S & w = Sum (S | 0) implies w is INT -valued )
S | Z = <*> the carrier of (Polynom-Ring (O,F_Real)) ;
then Sum (S | Z) = 0. (Polynom-Ring (O,F_Real)) by RLVECT_1:43
.= 0_ (O,F_Real) by POLYNOM1:def 11 ;
hence ( 0 <= len S & w = Sum (S | 0) implies w is INT -valued ) ; :: thesis: verum

end;

A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
let w be Polynomial of O,F_Real; :: thesis: ( i + 1 <= len S & w = Sum (S | (i + 1)) implies w is INT -valued )
assume A6: ( i + 1 <= len S & w = Sum (S | (i + 1)) ) ; :: thesis: w is INT -valued
A7: i < len S by A6, NAT_1:13;
A8: i + 1 in dom S by A6, FINSEQ_3:25, NAT_1:11;
S . (i + 1) = (p . ((SgmX ((BagOrder O),(Support p))) /. (i + 1))) * (Subst (((SgmX ((BagOrder O),(Support p))) /. (i + 1)),x,s)) by A8, A2;
then reconsider Si1 = S /. (i + 1) as INT -valued Polynomial of O,F_Real by A8, PARTFUN1:def 6;
reconsider SU = Sum (S | i) as Polynomial of O,F_Real by POLYNOM1:def 11;
A9: SU is INT -valued by A5, A7;
S | (i + 1) = (S | i) ^ <*(S /. (i + 1))*> by A6, FINSEQ_5:82;
then w = (Sum (S | i)) + (Sum <*(S /. (i + 1))*>) by A6, RLVECT_1:41
.= (Sum (S | i)) + (S /. (i + 1)) by RLVECT_1:44
.= SU + Si1 by POLYNOM1:def 11 ;
hence w is INT -valued by A9; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
then S₁[ len S] ;
hence Subst (p,x,s) is INT -valued by A1; :: thesis: verum