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