let i, j be 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 CARD_1:def 7;
then j in dom (- R) by FINSEQ_1:def 3;
hence ( not a = R . j or (- R) . j = - a ) by Th22; :: thesis: verum