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 (p extended_by_0) . (b bag_extend 0) = p . b
let b be bag of n; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds (p extended_by_0) . (b bag_extend 0) = p . b
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds (p extended_by_0) . (b bag_extend 0) = p . b
let p be Series of n,L; :: thesis: (p extended_by_0) . (b bag_extend 0) = p . b
(b bag_extend 0) . n = 0 by HILBASIS:def 1;
hence (p extended_by_0) . (b bag_extend 0) = p . ((0,n) -cut (b bag_extend 0)) by Def3
.= p . b by Th5 ;
:: thesis: verum