let
K
be
Field
;
:: thesis:
for
M1
,
M2
,
M3
being
Matrix
of
K
st

M1
=

M2
holds
M1
=
M2
let
M1
,
M2
,
M3
be
Matrix
of
K
;
:: thesis:
(

M1
=

M2
implies
M1
=
M2
)
assume

M1
=

M2
;
:: thesis:
M1
=
M2
then

(

M1
)
=
M2
by
Th1
;
hence
M1
=
M2
by
Th1
;
:: thesis:
verum