let x be object ; :: thesis:
let X be Ordinal; :: thesis:
let S be non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr ; :: thesis:
let p be Polynomial of X,S; :: thesis:
let t be bag of X; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in vars (Subst (t,x,p)) ; :: thesis:
then consider b being bag of X such that
A1: ( b in Support (Subst (t,x,p)) & b . y <> 0 ) by Def5;
A2: (Subst (t,x,p)) . b <> 0. S by A1, POLYNOM1:def 3;
then consider s being bag of X such that
A3: b = Subst (t,x,s) by Def3;
A4: ( y in dom b & dom b = X & X = dom t ) by A1, FUNCT_1:def 2, PARTFUN1:def 2;
A5: ( s in Bags X & Bags X = dom (p `^ (t . x)) ) by PRE_POLY:def 12, PARTFUN1:def 2;
b . y = ((t +* (x,0)) . y) + (s . y) by A3, PRE_POLY:def 5;

per cases ) . y <> 0 or s . y <> 0 ) by A1;

suppose A6: (t +* (x,0)) . y <> 0 ; :: thesis:

then A7: y <> x by A4, FUNCT_7:31;
then (t +* (x,0)) . y = t . y by FUNCT_7:32;
then y in support t by A6, PRE_POLY:def 7;
then y in (support t) \ {x} by A7, ZFMISC_1:56;
hence y in ((support t) \ {x}) \/ (vars p) by XBOOLE_0:def 3; :: thesis:

end;

suppose A8: s . y <> 0 ; :: thesis:

(p `^ (t . x)) . s <> 0. S by A2, A3, Def3;
then s in Support (p `^ (t . x)) by A5, POLYNOM1:def 4;
then ( y in vars (p `^ (t . x)) & vars (p `^ (t . x)) c= vars p ) by A8, Def5, Th45;
hence y in ((support t) \ {x}) \/ (vars p) by XBOOLE_0:def 3; :: thesis:

end;

end;