let n, m be Nat; :: thesis: for K being Ring
for A being Matrix of n,m,K holds A + (- A) = 0. (K,n,m)
let K be Ring; :: 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: width (- A) = width A by MATRIX_1:def 4;
A2: len (A + (- A)) = len A by MATRIX_1:def 6;
A3: width (A + (- A)) = width A by MATRIX_1:def 6;
A4: len (- A) = len A by MATRIX_1:def 4;

A5: now :: thesis: ( ( n > 0 & 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)) ) or ( n = 0 & 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)) ) )

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

case A6: 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 ( len (A + (- A)) = n & width (A + (- A)) = m ) by MATRIX_0:23;
hence ( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) ) by A6, MATRIX_0:23; :: thesis: ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
( dom A = dom (- A) & dom A = dom (A + (- A)) ) by A4, A2, FINSEQ_3:29;
hence ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) by A1, A3; :: thesis: verum

end;

case A7: 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 A8: width A = 0 by MATRIX_0:22;
then A9: Seg (width (- A)) = Seg 0 by A1;
A10: len A = 0 by A7, MATRIX_0:22;
then A11: dom (- A) = Seg 0 by A4, FINSEQ_1:def 3;
A12: Indices (- A) = [:(Seg 0),(Seg 0):] by A9, A11;
dom (A + (- A)) = Seg 0 by A2, A10, FINSEQ_1:def 3;
then A13: Indices (A + (- A)) = [:(Seg 0),(Seg 0):] by A3, A8;
( len (0. (K,n,m)) = 0 & width (0. (K,n,m)) = 0 ) by A7, MATRIX_0:22;
hence ( len (0. (K,n,m)) = len (A + (- A)) & width (0. (K,n,m)) = width (A + (- A)) ) by A10, A8, MATRIX_1:def 6; :: thesis: ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) )
Indices A = {} by A7, MATRIX_0:22;
hence ( Indices A = Indices (- A) & Indices A = Indices (A + (- A)) ) by A12, A13, ZFMISC_1:90; :: thesis: verum

end;

end;

end;

A14: Indices A = Indices (0. (K,n,m)) by MATRIX_0:26;

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

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies (A + (- A)) * (i,j) = (0. (K,n,m)) * (i,j) )
assume A15: [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 MATRIX_1:def 6
.= (A * (i,j)) + (- (A * (i,j))) by A15, MATRIX_1:def 4
.= 0. K by RLVECT_1:5
.= (0. (K,n,m)) * (i,j) by A14, A15, Th1 ;
:: thesis: verum

end;

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