theorem :: MATRIX_3:38

for K being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for A being Matrix of K holds A * (- (1. K)) = - A