let n be Ordinal; :: thesis: for b, b' being bag of n
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 n; :: 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 PRE_POLY:50;
hence (b *' p) . (b' + b) = p . ((b' + b) -' b) by Def1
.= p . b' by PRE_POLY:48 ;
:: thesis: verum