let x be object ; :: thesis: for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p, s being Polynomial of X,S holds vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s)
let X be Ordinal; :: thesis: for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p, s being Polynomial of X,S holds vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s)
let S be non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr ; :: thesis: for p, s being Polynomial of X,S holds vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s)
let p, s be Polynomial of X,S; :: thesis: vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s)
set PR = Polynom-Ring (X,S);
set SX = SgmX ((BagOrder X),(Support p));
consider F being FinSequence of (Polynom-Ring (X,S)) such that
A1: ( Subst (p,x,s) = Sum F & len (SgmX ((BagOrder X),(Support p))) = len F ) and
A2: for i being Nat st i in dom F holds
F . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) by Def4;
defpred S₁[ Nat] means for i being Nat st i = $1 & i <= len F holds
for q being Polynomial of X,S st q = Sum (F | i) holds
vars q c= ((vars p) \ {x}) \/ (vars s);
A3: S₁[ 0 ]

proof

let i be Nat; :: thesis: ( i = 0 & i <= len F implies for q being Polynomial of X,S st q = Sum (F | i) holds
vars q c= ((vars p) \ {x}) \/ (vars s) )
assume A4: ( i = 0 & i <= len F ) ; :: thesis: for q being Polynomial of X,S st q = Sum (F | i) holds
vars q c= ((vars p) \ {x}) \/ (vars s)
let q be Polynomial of X,S; :: thesis: ( q = Sum (F | i) implies vars q c= ((vars p) \ {x}) \/ (vars s) )
assume A5: q = Sum (F | i) ; :: thesis: vars q c= ((vars p) \ {x}) \/ (vars s)
F | i = <*> the carrier of (Polynom-Ring (X,S)) by A4;
then q = 0. (Polynom-Ring (X,S)) by A5, RLVECT_1:43
.= 0_ (X,S) by POLYNOM1:def 11 ;
hence vars q c= ((vars p) \ {x}) \/ (vars s) by Th38; :: thesis: verum

end;

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]
let n1 be Nat; :: thesis: ( n1 = n + 1 & n1 <= len F implies for q being Polynomial of X,S st q = Sum (F | n1) holds
vars q c= ((vars p) \ {x}) \/ (vars s) )
assume A8: ( n1 = n + 1 & n1 <= len F ) ; :: thesis: for q being Polynomial of X,S st q = Sum (F | n1) holds
vars q c= ((vars p) \ {x}) \/ (vars s)
let q be Polynomial of X,S; :: thesis: ( q = Sum (F | n1) implies vars q c= ((vars p) \ {x}) \/ (vars s) )
assume A9: q = Sum (F | n1) ; :: thesis: vars q c= ((vars p) \ {x}) \/ (vars s)
reconsider q1 = Sum (F | n), Fn1 = F /. n1 as Polynomial of X,S by POLYNOM1:def 11;
A10: ( n1 in dom F & n1 in dom (SgmX ((BagOrder X),(Support p))) ) by A1, A8, FINSEQ_3:25, NAT_1:11;
then A11: ( F | n1 = (F | n) ^ <*(F . n1)*> & F . n1 = F /. n1 & (SgmX ((BagOrder X),(Support p))) . n1 = (SgmX ((BagOrder X),(Support p))) /. n1 ) by A8, FINSEQ_5:10, PARTFUN1:def 6;
then q = (Sum (F | n)) + (Sum <*(F /. n1)*>) by A9, RLVECT_1:41
.= (Sum (F | n)) + (F /. n1) by RLVECT_1:44
.= q1 + Fn1 by POLYNOM1:def 11 ;
then A12: vars q c= (vars q1) \/ (vars Fn1) by Th41;
n < len F by NAT_1:13, A8;
then A13: vars q1 c= ((vars p) \ {x}) \/ (vars s) by A7;
Fn1 = (p . ((SgmX ((BagOrder X),(Support p))) /. n1)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. n1),x,s)) by A11, A2, A10;
then A14: vars Fn1 c= vars (Subst (((SgmX ((BagOrder X),(Support p))) /. n1),x,s)) by Th44;
A15: vars (Subst (((SgmX ((BagOrder X),(Support p))) /. n1),x,s)) c= ((support ((SgmX ((BagOrder X),(Support p))) /. n1)) \ {x}) \/ (vars s) by Th46;
BagOrder X linearly_orders Support p by POLYNOM2:18;
then ( (SgmX ((BagOrder X),(Support p))) /. n1 in rng (SgmX ((BagOrder X),(Support p))) & rng (SgmX ((BagOrder X),(Support p))) = Support p ) by A10, A11, PRE_POLY:def 2, FUNCT_1:def 3;
then (support ((SgmX ((BagOrder X),(Support p))) /. n1)) \ {x} c= (vars p) \ {x} by Th40, XBOOLE_1:33;
then ((support ((SgmX ((BagOrder X),(Support p))) /. n1)) \ {x}) \/ (vars s) c= ((vars p) \ {x}) \/ (vars s) by XBOOLE_1:9;
then vars Fn1 c= ((vars p) \ {x}) \/ (vars s) by A14, A15;
then (vars q1) \/ (vars Fn1) c= ((vars p) \ {x}) \/ (vars s) by A13, XBOOLE_1:8;
hence vars q c= ((vars p) \ {x}) \/ (vars s) by A12; :: thesis: verum

end;

A16: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
F | (len F) = F ;
hence vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s) by A1, A16; :: thesis: verum