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 A1: ( len A = n & width A = m & n > 0 ) ; :: thesis: ( A + (0_Rmatrix n,m) = A & (0_Rmatrix n,m) + A = A )
then A2: ( len (0. F_Real ,n,m) = n & width (0. F_Real ,n,m) = m ) by MATRIX_1:24;
A3: MXR2MXF A is Matrix of n,m,F_Real by A1, MATRIX_1:20;
reconsider D = MXR2MXF A as Matrix of n,m,F_Real by A1, MATRIX_1:20;
(0_Rmatrix n,m) + A = MXF2MXR (D + (0. F_Real ,n,m)) by A1, A2, MATRIX_3:4
.= A by MATRIX_3:6 ;
hence ( A + (0_Rmatrix n,m) = A & (0_Rmatrix n,m) + A = A ) by A3, MATRIX_3:6; :: thesis: verum