let n be Nat; :: thesis: for L being non empty ZeroStr
for p being Series of n,L
for b being bag of n + 1 st b in Support (p extended_by_0) holds
b . n = 0
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L
for b being bag of n + 1 st b in Support (p extended_by_0) holds
b . n = 0
let p be Series of n,L; :: thesis: for b being bag of n + 1 st b in Support (p extended_by_0) holds
b . n = 0
let b be bag of n + 1; :: thesis: ( b in Support (p extended_by_0) implies b . n = 0 )
assume b in Support (p extended_by_0) ; :: thesis: b . n = 0
then (p extended_by_0) . b <> 0. L by POLYNOM1:def 3;
hence b . n = 0 by Def3; :: thesis: verum