let n, m be Nat; :: thesis: for K being Field
for A being Matrix of n,m,K holds A + (- A) = 0. K,n,m
let K be Field; :: thesis: for A being Matrix of n,m,K holds A + (- A) = 0. K,n,m
let A be Matrix of n,m,K; :: thesis: A + (- A) = 0. K,n,m
A1: ( len (- A) = len A & width (- A) = width A ) by Def2;
A2: ( len (A + (- A)) = len A & width (A + (- A)) = width A ) by Def3;
A3: Indices A = Indices (0. K,n,m) by MATRIX_1:27;

A4: now

per cases ( n > 0 or n = 0 ) ;

case A5: n > 0 ; :: thesis: ( len (0. K,n,m) = len (A + (- A)) & width (0. K,n,m) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )

then A6: ( len A = n & width A = m & Indices A = [:(Seg n),(Seg m):] ) by MATRIX_1:24;
( len (- A) = n & width (- A) = m & len (A + (- A)) = n & width (A + (- A)) = m & len (0. K,n,m) = n & width (0. K,n,m) = m ) by A1, A2, A5, MATRIX_1:24;
hence ( len (0. K,n,m) = len (A + (- A)) & width (0. K,n,m) = width (A + (- A)) ) ; :: thesis: ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
( Seg n = dom A & dom A = dom (- A) & dom A = dom (A + (- A)) ) by A1, A2, A6, FINSEQ_1:def 3, FINSEQ_3:31;
hence ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) by A1, A2, A6, MATRIX_1:def 5; :: thesis: verum

end;

case n = 0 ; :: thesis: ( len (0. K,n,m) = len (A + (- A)) & width (0. K,n,m) = width (A + (- A)) & Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )

then A7: ( len A = 0 & width A = 0 & Indices A = {} & len (0. K,n,m) = 0 & width (0. K,n,m) = 0 ) by MATRIX_1:23;
hence ( len (0. K,n,m) = len (A + (- A)) & width (0. K,n,m) = width (A + (- A)) ) by Def3; :: thesis: ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
( dom (- A) = Seg 0 & dom (A + (- A)) = Seg 0 ) by A1, A2, A7, FINSEQ_1:def 3;
then ( Indices (- A) = [:(Seg 0 ),(Seg 0 ):] & Indices (A + (- A)) = [:(Seg 0 ),(Seg 0 ):] ) by A1, A2, A7, MATRIX_1:def 5;
hence ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) by A7, FINSEQ_1:4, ZFMISC_1:113; :: thesis: verum

end;

end;

end;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies (A + (- A)) * i,j = (0. K,n,m) * i,j )
assume A8: [i,j] in Indices A ; :: thesis: (A + (- A)) * i,j = (0. K,n,m) * i,j
hence (A + (- A)) * i,j = (A * i,j) + ((- A) * i,j) by Def3
.= (A * i,j) + (- (A * i,j)) by A8, Def2
.= 0. K by RLVECT_1:16
.= (0. K,n,m) * i,j by A3, A8, Th3 ;
:: thesis: verum

end;

hence A + (- A) = 0. K,n,m by A4, MATRIX_1:21; :: thesis: verum