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

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

let 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;

hence p - p = 0_. L ; :: thesis: verum