let i be Nat; :: thesis: for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K holds - (R1 - R2) = R2 - R1
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: - (R1 - R2) = R2 - R1
thus - (R1 - R2) = - (R1 + (- R2)) by FINSEQOP:84
.= (- R1) + (- (- R2)) by Th31
.= (- R1) + R2 by Th28
.= R2 + (- R1) by FINSEQOP:33
.= R2 - R1 by FINSEQOP:84 ; :: thesis: verum