let L be non empty right_zeroed addLoopStr ; :: thesis: for p being sequence of L holds p + (0_. L) = p
let p be sequence of L; :: thesis: p + (0_. L) = p

now :: thesis: for n being Element of NAT holds (p + (0_. L)) . n = p . n

let n be Element of NAT ; :: thesis: (p + (0_. L)) . n = p . n
thus (p + (0_. L)) . n = (p . n) + ((0_. L) . n) by NORMSP_1:def 2
.= (p . n) + (0. L) by FUNCOP_1:7
.= p . n by RLVECT_1:def 4 ; :: thesis: verum

end;

hence p + (0_. L) = p ; :: thesis: verum