let K be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for A being Matrix of K holds A * (- (1. K)) = - A
let A be Matrix of K; :: thesis: A * (- (1. K)) = - A
A1: ( len (- A) = len A & width (- A) = width A ) by MATRIX_1:def 4;

now :: thesis: for i, j being Nat st [i,j] in Indices A holds
(- A) * (i,j) = (A * (i,j)) * (- (1. K))

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies (- A) * (i,j) = (A * (i,j)) * (- (1. K)) )
assume [i,j] in Indices A ; :: thesis: (- A) * (i,j) = (A * (i,j)) * (- (1. K))
hence (- A) * (i,j) = - ((A * (i,j)) * (1. K)) by MATRIX_1:def 4
.= (A * (i,j)) * (- (1. K)) by VECTSP_1:8 ;
:: thesis: verum

end;

hence A * (- (1. K)) = - A by A1, Def6; :: thesis: verum