let K be non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for A being Matrix of K holds (- (1. K)) * A = - A
let A be Matrix of K; :: thesis: (- (1. K)) * A = - 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) = (- (1. K)) * (A * (i,j))

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

end;

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