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 A1: n > 0 ; :: thesis: A + (0. (K,n,m)) = A

A3: width A = width (A + (0. (K,n,m))) by Def3;
A5: Indices A = [:(Seg n),(Seg m):] by A1, MATRIX_1:24;
A6: len A = len (A + (0. (K,n,m))) by Def3;
then dom A = dom (A + (0. (K,n,m))) by FINSEQ_3:31;
then A7: Indices A = Indices (A + (0. (K,n,m))) by A3;
A8: Indices (0. (K,n,m)) = [:(Seg n),(Seg m):] by A1, MATRIX_1:24;

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 A9: [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 A7, Def3
.= (A * (i,j)) + (0. K) by A5, A8, A7, A9, Th3
.= A * (i,j) by RLVECT_1:10 ;
:: thesis: verum

end;

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

end;

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

A11: width A = width (A + (0. (K,n,m))) by Def3;
A12: len A = len (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 A11;
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 A10, MATRIX_1:23;
hence A + (0. (K,n,m)) = A by A12, A11, MATRIX_1:21; :: thesis: verum

end;

end;