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