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 holds R1 - (- R2) = 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 holds R1 - (- R2) = R1 + R2
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: R1 - (- R2) = R1 + R2
thus R1 - (- R2) = R1 + (- (- R2)) by FINSEQOP:84
.= R1 + R2 by Th28 ; :: thesis: verum