let n be set ; 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 ; for p being Series of n,L holds (0_ (n,L)) + p = p
let p be Series of n,L; (0_ (n,L)) + p = p
reconsider ls = (0_ (n,L)) + p, p9 = p as Function of (Bags n), the carrier of L ;
hence
(0_ (n,L)) + p = p
by FUNCT_2:63; verum