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

proof

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

end;

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