let R be Ring; :: thesis: for A being Matrix of R
for r being Element of R holds (- r) * A = - (r * A)
let A be Matrix of R; :: thesis: for r being Element of R holds (- r) * A = - (r * A)
let r be Element of R; :: thesis: (- r) * A = - (r * A)
A1: ( len ((- r) * A) = len A & len (- (r * A)) = len A & len (r * A) = len A )

proof

thus len ((- r) * A) = len A by MATRIX_3:def 5; :: thesis: ( len (- (r * A)) = len A & len (r * A) = len A )
thus len (- (r * A)) = len (r * A) by MATRIX_1:def 4
.= len A by MATRIX_3:def 5 ; :: thesis: len (r * A) = len A
thus len (r * A) = len A by MATRIX_3:def 5; :: thesis: verum

end;

A2: ( width ((- r) * A) = width A & width (- (r * A)) = width A & width (r * A) = width A )

proof

thus width ((- r) * A) = width A by MATRIX_3:def 5; :: thesis: ( width (- (r * A)) = width A & width (r * A) = width A )
thus width (- (r * A)) = width (r * A) by MATRIX_1:def 4
.= width A by MATRIX_3:def 5 ; :: thesis: width (r * A) = width A
thus width (r * A) = width A by MATRIX_3:def 5; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices ((- r) * A) holds
((- r) * A) * (i,j) = (- (r * A)) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices ((- r) * A) implies ((- r) * A) * (i,j) = (- (r * A)) * (i,j) )
assume A3: [i,j] in Indices ((- r) * A) ; :: thesis: ((- r) * A) * (i,j) = (- (r * A)) * (i,j)
A4: Indices ((- r) * A) = [:(dom ((- r) * A)),(Seg (width ((- r) * A))):] by MATRIX_0:def 4
.= [:(Seg (len ((- r) * A))),(Seg (width ((- r) * A))):] by FINSEQ_1:def 3
.= [:(dom A),(Seg (width A)):] by A1, A2, FINSEQ_1:def 3
.= Indices A by MATRIX_0:def 4 ;
A5: Indices A = [:(dom A),(Seg (width A)):] by MATRIX_0:def 4
.= [:(Seg (len A)),(Seg (width A)):] by FINSEQ_1:def 3
.= [:(dom (r * A)),(Seg (width (r * A))):] by A1, A2, FINSEQ_1:def 3
.= Indices (r * A) by MATRIX_0:def 4 ;
thus ((- r) * A) * (i,j) = (- r) * (A * (i,j)) by A3, A4, MATRIX_3:def 5
.= - (r * (A * (i,j))) by VECTSP_1:9
.= - ((r * A) * (i,j)) by A3, A4, MATRIX_3:def 5
.= (- (r * A)) * (i,j) by A3, A4, A5, MATRIX_1:def 4 ; :: thesis: verum

end;

hence (- r) * A = - (r * A) by A1, A2, MATRIX_0:21; :: thesis: verum