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

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 6
.= 0. L by RLVECT_1:28
.= (0_. L) . n by FUNCOP_1:13 ; :: thesis: verum

end;

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