let n, m be Nat; :: thesis: for K being Field
for A being Matrix of n,m,K holds A + (0. K,n,m) = A
let K be Field; :: thesis: for A being Matrix of n,m,K holds A + (0. K,n,m) = A
let A be Matrix of n,m,K; :: thesis: A + (0. K,n,m) = A

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

suppose n > 0 ; :: thesis: A + (0. K,n,m) = A

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

now

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

end;

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

end;

suppose A5: n = 0 ; :: thesis: A + (0. K,n,m) = A

A6: ( len A = len (A + (0. K,n,m)) & width A = width (A + (0. K,n,m)) ) by Def3;
then dom A = dom (A + (0. K,n,m)) by FINSEQ_3:31;
then ( Indices A = [:(dom A),(Seg (width A)):] & Indices (A + (0. K,n,m)) = [:(dom A),(Seg (width A)):] ) by A6, MATRIX_1:def 5;
then for i, j being Nat st [i,j] in Indices (A + (0. K,n,m)) holds
(A + (0. K,n,m)) * i,j = A * i,j by A5, MATRIX_1:23;
hence A + (0. K,n,m) = A by A6, MATRIX_1:21; :: thesis: verum

end;

end;