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

now

let b be Element of Bags n; :: thesis: ls . b = p9 . b
thus ls . b = (p . b) + ((0_ n,L) . b) by Def21
.= (p9 . b) + (0. L) by Th81
.= p9 . b by RLVECT_1:def 7 ; :: thesis: verum

end;

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