let i be Nat; :: thesis: for K being non empty addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
let K be non empty addLoopStr ; :: thesis: for a being Element of K
for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
let a be Element of K; :: thesis: for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a
let p be FinSequence of the carrier of K; :: thesis: ( i in dom (- p) & a = p . i implies (- p) . i = - a )
assume ( i in dom (- p) & a = p . i ) ; :: thesis: (- p) . i = - a
then (- p) . i = (comp K) . a by FUNCT_1:12;
hence (- p) . i = - a by VECTSP_1:def 13; :: thesis: verum