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