let A, B be Matrix of REAL ; :: thesis: ( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A + B) * i,j = (A * i,j) + (B * i,j) ) )
thus ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def 3; :: thesis: for i, j being Nat st [i,j] in Indices A holds
(A + B) * i,j = (A * i,j) + (B * i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices A implies (A + B) * i,j = (A * i,j) + (B * i,j) )
assume [i,j] in Indices A ; :: thesis: (A + B) * i,j = (A * i,j) + (B * i,j)
then (A + B) * i,j = ((MXR2MXF A) * i,j) + ((MXR2MXF B) * i,j) by MATRIX_3:def 3;
hence (A + B) * i,j = (A * i,j) + (B * i,j) ; :: thesis: verum