len
(
M1
+
(

M2
)
)
=
len
M1
by
MATRIX_3:def 3
;
hence
M1

M2
is
Matrix
of
n
,
REAL
by
MATRIX_4:def 1
;
:: thesis:
verum