len
M
=
n
by
MATRIX_0:24
;
then
A1
:
len
|:
M
:|
=
n
by
Def7
;
width
M
=
n
by
MATRIX_0:24
;
then
width
|:
M
:|
=
n
by
Def7
;
hence
|:
M
:|
is
Matrix
of
n
,
REAL
by
A1
,
MATRIX_0:51
;
:: thesis:
verum