let j, i be Element of NAT ; :: thesis: for K being non empty addLoopStr
for a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
let K be non empty addLoopStr ; :: thesis: for a being Element of K
for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
let a be Element of K; :: thesis: for R being Element of i -tuples_on the carrier of K st j in Seg i & a = R . j holds
(- R) . j = - a
let R be Element of i -tuples_on the carrier of K; :: thesis: ( j in Seg i & a = R . j implies (- R) . j = - a )
assume j in Seg i ; :: thesis: ( not a = R . j or (- R) . j = - a )
then j in Seg (len (- R)) by FINSEQ_1:def 18;
then j in dom (- R) by FINSEQ_1:def 3;
hence ( not a = R . j or (- R) . j = - a ) by Th30; :: thesis: verum