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

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

hence
p + (0_. L) = p
; :: thesis: verumlet 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;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