let n be Nat; :: thesis: for b being bag of n
for L being non empty ZeroStr
for p being Series of n,L holds
( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )
let b be bag of n; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds
( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds
( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )
let p be Series of n,L; :: thesis: ( b bag_extend 0 in Support (p extended_by_0) iff b in Support p )
set B = b bag_extend 0;
set P = p extended_by_0 ;
(b bag_extend 0) . n = 0 by HILBASIS:def 1;
then A1: (p extended_by_0) . (b bag_extend 0) = p . ((0,n) -cut (b bag_extend 0)) by Def3
.= p . b by Th5 ;
thus ( b bag_extend 0 in Support (p extended_by_0) implies b in Support p ) :: thesis: ( b in Support p implies b bag_extend 0 in Support (p extended_by_0) )

proof

assume b bag_extend 0 in Support (p extended_by_0) ; :: thesis: b in Support p
then ( p . b <> 0. L & b in Bags n & dom p = Bags n ) by POLYNOM1:def 3, A1, FUNCT_2:def 1, PRE_POLY:def 12;
hence b in Support p by POLYNOM1:def 3; :: thesis: verum

end;

assume b in Support p ; :: thesis: b bag_extend 0 in Support (p extended_by_0)
then A2: p . b <> 0. L by POLYNOM1:def 3;
( b bag_extend 0 in Bags (n + 1) & dom (p extended_by_0) = Bags (n + 1) ) by FUNCT_2:def 1;
hence b bag_extend 0 in Support (p extended_by_0) by POLYNOM1:def 3, A2, A1; :: thesis: verum