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

then len A = n by MATRIX_1:24;
then A2: Seg n = dom A by FINSEQ_1:def 3;
A3: width A = width (A + (0. K,n,m)) by Def3;
A4: width A = m by A1, MATRIX_1:24;
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 A4, A5, A3, A2, MATRIX_1:def 5;
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, 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 A10, MATRIX_1:23;
hence A + (0. K,n,m) = A by A12, A11, MATRIX_1:21; :: thesis: verum

end;

end;