let n be Nat; :: thesis: for x being object
for X being set
for S being non empty ZeroStr
for s being Element of S holds vars (Monom (s,((EmptyBag X) +* (x,n)))) c= {x}
let x be object ; :: thesis: for X being set
for S being non empty ZeroStr
for s being Element of S holds vars (Monom (s,((EmptyBag X) +* (x,n)))) c= {x}
let X be set ; :: thesis: for S being non empty ZeroStr
for s being Element of S holds vars (Monom (s,((EmptyBag X) +* (x,n)))) c= {x}
let S be non empty ZeroStr ; :: thesis: for s being Element of S holds vars (Monom (s,((EmptyBag X) +* (x,n)))) c= {x}
let s be Element of S; :: thesis: vars (Monom (s,((EmptyBag X) +* (x,n)))) c= {x}
set EX = (EmptyBag X) +* (x,n);
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in vars (Monom (s,((EmptyBag X) +* (x,n)))) or y in {x} )
assume y in vars (Monom (s,((EmptyBag X) +* (x,n)))) ; :: thesis: y in {x}
then consider b being bag of X such that
A1: ( b in Support (Monom (s,((EmptyBag X) +* (x,n)))) & b . y <> 0 ) by Def5;
assume not y in {x} ; :: thesis: contradiction
then A2: y <> x by TARSKI:def 1;
Support (Monom (s,((EmptyBag X) +* (x,n)))) = {(term (Monom (s,((EmptyBag X) +* (x,n)))))} by A1, POLYNOM7:7;
then A3: b = term (Monom (s,((EmptyBag X) +* (x,n)))) by TARSKI:def 1, A1;
coefficient (Monom (s,((EmptyBag X) +* (x,n)))) <> 0. S by A1, POLYNOM7:def 5;
then s <> 0. S by POLYNOM7:8;
then ( not s is zero & S is non trivial ZeroStr ) by STRUCT_0:def 12, STRUCT_0:def 18;
then b = (EmptyBag X) +* (x,n) by A3, POLYNOM7:10;
then b . y = (EmptyBag X) . y by A2, FUNCT_7:32;
hence contradiction by A1; :: thesis: verum