let n, m be Nat; :: thesis: for A being Matrix of REAL st len A = n & width A = m & n > 0 holds

( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )

let A be Matrix of REAL; :: thesis: ( len A = n & width A = m & n > 0 implies ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) )

assume that

A1: ( len A = n & width A = m ) and

A2: n > 0 ; :: thesis: ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )

reconsider D = MXR2MXF A as Matrix of n,m,F_Real by A1, A2, MATRIX_0:20;

( len (0. (F_Real,n,m)) = n & width (0. (F_Real,n,m)) = m ) by A2, MATRIX_0:23;

then A3: (0_Rmatrix (n,m)) + A = MXF2MXR (D + (0. (F_Real,n,m))) by A1, MATRIX_3:2

.= A by MATRIX_3:4 ;

MXR2MXF A is Matrix of n,m,F_Real by A1, A2, MATRIX_0:20;

hence ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) by A3, MATRIX_3:4; :: thesis: verum

( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )

let A be Matrix of REAL; :: thesis: ( len A = n & width A = m & n > 0 implies ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) )

assume that

A1: ( len A = n & width A = m ) and

A2: n > 0 ; :: thesis: ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )

reconsider D = MXR2MXF A as Matrix of n,m,F_Real by A1, A2, MATRIX_0:20;

( len (0. (F_Real,n,m)) = n & width (0. (F_Real,n,m)) = m ) by A2, MATRIX_0:23;

then A3: (0_Rmatrix (n,m)) + A = MXF2MXR (D + (0. (F_Real,n,m))) by A1, MATRIX_3:2

.= A by MATRIX_3:4 ;

MXR2MXF A is Matrix of n,m,F_Real by A1, A2, MATRIX_0:20;

hence ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) by A3, MATRIX_3:4; :: thesis: verum