let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being sequence of L holds p - p = 0_. L

let p be sequence of L; :: thesis: p - p = 0_. L

let p be sequence of L; :: thesis: p - p = 0_. L

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

hence
p - p = 0_. L
; :: thesis: verumlet n be Element of NAT ; :: thesis: (p - p) . n = (0_. L) . n

thus (p - p) . n = (p . n) - (p . n) by NORMSP_1:def 3

.= 0. L by RLVECT_1:15

.= (0_. L) . n by FUNCOP_1:7 ; :: thesis: verum

end;thus (p - p) . n = (p . n) - (p . n) by NORMSP_1:def 3

.= 0. L by RLVECT_1:15

.= (0_. L) . n by FUNCOP_1:7 ; :: thesis: verum