let i be Nat; :: thesis: for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds
R1 = R2
let K be non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr ; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K st - R1 = - R2 holds
R1 = R2
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( - R1 = - R2 implies R1 = R2 )
assume - R1 = - R2 ; :: thesis: R1 = R2
hence R1 = - (- R2) by Th28
.= R2 by Th28 ;
:: thesis: verum