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