let n be Ordinal; :: thesis: for b, b' being bag of
for L being non empty ZeroStr
for p being Series of n,L holds (b *' p) . (b' + b) = p . b'
let b, b' be bag of ; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds (b *' p) . (b' + b) = p . b'
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds (b *' p) . (b' + b) = p . b'
let p be Series of n,L; :: thesis: (b *' p) . (b' + b) = p . b'
b divides b' + b by POLYNOM1:54;
hence (b *' p) . (b' + b) = p . ((b' + b) -' b) by Def1
.= p . b' by POLYNOM1:52 ;
:: thesis: verum