let L be non empty addLoopStr ; :: thesis: for p, q being sequence of L holds p - q = p + (- q)
let p, q be sequence of L; :: thesis: p - q = p + (- q)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (p - q) . n = (p + (- q)) . n
thus (p - q) . n = (p . n) - (q . n) by NORMSP_1:def 3
.= (p . n) + ((- q) . n) by BHSP_1:44
.= (p + (- q)) . n by NORMSP_1:def 2 ; :: thesis: verum