let i be Nat; :: thesis: for K being non empty addLoopStr
for a being Element of K holds - (i |-> a) = i |-> (- a)
let K be non empty addLoopStr ; :: thesis: for a being Element of K holds - (i |-> a) = i |-> (- a)
let a be Element of K; :: thesis: - (i |-> a) = i |-> (- a)
thus - (i |-> a) = i |-> ((comp K) . a) by FINSEQOP:16
.= i |-> (- a) by VECTSP_1:def 13 ; :: thesis: verum