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

proof

let i be Element of Bags n; :: thesis: ((1. L) * p) . i = p . i
thus ((1. L) * p) . i = (1. L) * (p . i) by POLYNOM7:def 9
.= p . i ; :: thesis: verum

end;

hence (1. L) * p = p ; :: thesis: verum