let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Series of (n + 1),L holds vars (p removed_last) c= (vars p) \ {n}
let L be non empty ZeroStr ; :: thesis: for p being Series of (n + 1),L holds vars (p removed_last) c= (vars p) \ {n}
let p be Series of (n + 1),L; :: thesis: vars (p removed_last) c= (vars p) \ {n}
set r = p removed_last ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in vars (p removed_last) or y in (vars p) \ {n} )
assume y in vars (p removed_last) ; :: thesis: y in (vars p) \ {n}
then consider b being bag of n such that
A1: ( b in Support (p removed_last) & b . y <> 0 ) by Def5;
set bn = b bag_extend 0;
A2: Bags (n + 1) = dom p by PARTFUN1:def 2;
( 0. L <> (p removed_last) . b & (p removed_last) . b = p . (b bag_extend 0) & b bag_extend 0 in Bags (n + 1) ) by A1, Def6, POLYNOM1:def 4;
then A3: b bag_extend 0 in Support p by POLYNOM1:def 3, A2;
A4: ( y in dom b & dom b = n ) by A1, FUNCT_1:def 2, PARTFUN1:def 2;
then ((b bag_extend 0) | n) . y = (b bag_extend 0) . y by FUNCT_1:49;
then b . y = (b bag_extend 0) . y by HILBASIS:def 1;
then A5: y in vars p by A3, A1, Def5;
not n in n ;
hence y in (vars p) \ {n} by A4, A5, ZFMISC_1:56; :: thesis: verum