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