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: width (- A) = width A by Def2;
A2: len (A + (- A)) = len A by Def3;
A3: width (A + (- A)) = width A by Def3;
A4: len (- A) = len A by Def2;

A5: now

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

end;

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

end;

end;

end;

A14: Indices A = Indices (0. (K,n,m)) by MATRIX_1:27;

now

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 Def3
.= (A * (i,j)) + (- (A * (i,j))) by A15, Def2
.= 0. K by RLVECT_1:16
.= (0. (K,n,m)) * (i,j) by A14, A15, Th3 ;
:: thesis: verum

end;

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