let
K
be
Field
;
:: thesis:
for
A
,
B
being
Matrix
of
K
holds
Indices
(
A
+
B
)
=
Indices
A
let
A
,
B
be
Matrix
of
K
;
:: thesis:
Indices
(
A
+
B
)
=
Indices
A
(
len
(
A
+
B
)
=
len
A
&
width
(
A
+
B
)
=
width
A
)
by
MATRIX_3:def 3
;
hence
Indices
(
A
+
B
)
=
Indices
A
by
MATRIX_4:55
;
:: thesis:
verum