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