let n be Ordinal; :: thesis: for L being non degenerated comRing
for a, b being Element of L
for p being Series of n,L holds (a + b) * p = (a * p) + (b * p)
let L be non degenerated comRing; :: thesis: for a, b being Element of L
for p being Series of n,L holds (a + b) * p = (a * p) + (b * p)
let a, b be Element of L; :: thesis: for p being Series of n,L holds (a + b) * p = (a * p) + (b * p)
let p be Series of n,L; :: thesis: (a + b) * p = (a * p) + (b * p)
for i being Element of Bags n holds ((a + b) * p) . i = ((a * p) + (b * p)) . i

proof

let i be Element of Bags n; :: thesis: ((a + b) * p) . i = ((a * p) + (b * p)) . i
thus ((a + b) * p) . i = (a + b) * (p . i) by POLYNOM7:def 9
.= (a * (p . i)) + (b * (p . i)) by VECTSP_1:def 7
.= ((a * p) . i) + (b * (p . i)) by POLYNOM7:def 9
.= ((a * p) . i) + ((b * p) . i) by POLYNOM7:def 9
.= ((a * p) + (b * p)) . i by POLYNOM1:15 ; :: thesis: verum

end;

hence (a + b) * p = (a * p) + (b * p) ; :: thesis: verum