let n be set ; :: thesis: for L being non empty left_zeroed addLoopStr
for p being Series of n,L holds (0_ n,L) + p = p
let L be non empty left_zeroed addLoopStr ; :: thesis: for p being Series of n,L holds (0_ n,L) + p = p
let p be Series of n,L; :: thesis: (0_ n,L) + p = p
reconsider ls = (0_ n,L) + p, p' = p as Function of (Bags n),the carrier of L ;

now

let b be Element of Bags n; :: thesis: ls . b = p' . b
thus ls . b = ((0_ n,L) . b) + (p . b) by POLYNOM1:def 21
.= (0. L) + (p' . b) by POLYNOM1:81
.= p' . b by ALGSTR_1:def 5 ; :: thesis: verum

end;

hence (0_ n,L) + p = p by FUNCT_2:113; :: thesis: verum