theorem Th44: :: FVSUM_1:44
for i being Nat
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