let n, m be Nat; :: thesis: for K being Ring
for A being Matrix of n,m,K holds A + (0. (K,n,m)) = A
let K be Ring; :: 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 A1: n > 0 ; :: thesis: A + (0. (K,n,m)) = A

A2: width A = width (A + (0. (K,n,m))) by Def3;
A3: Indices A = [:(Seg n),(Seg m):] by A1, MATRIX_0:23;
A4: len A = len (A + (0. (K,n,m))) by Def3;
then dom A = dom (A + (0. (K,n,m))) by FINSEQ_3:29;
then A5: Indices A = Indices (A + (0. (K,n,m))) by A2;
A6: Indices (0. (K,n,m)) = [:(Seg n),(Seg m):] by A1, MATRIX_0:23;

now :: thesis: 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)

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 A7: [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 A5, Def3
.= (A * (i,j)) + (0. K) by A3, A6, A5, A7, Th1
.= A * (i,j) by RLVECT_1:4 ;
:: thesis: verum

end;

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

end;

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

A9: width A = width (A + (0. (K,n,m))) by Def3;
A10: len A = len (A + (0. (K,n,m))) by Def3;
then dom A = dom (A + (0. (K,n,m))) by FINSEQ_3:29;
then ( Indices A = [:(dom A),(Seg (width A)):] & Indices (A + (0. (K,n,m))) = [:(dom A),(Seg (width A)):] ) by A9;
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 A8, MATRIX_0:22;
hence A + (0. (K,n,m)) = A by A10, A9, MATRIX_0:21; :: thesis: verum

end;

end;