let M be Matrix of 3,REAL; ( M * (0_Rmatrix 3) = 0_Rmatrix 3 & (0_Rmatrix 3) * M = 0_Rmatrix 3 )
A1:
( width (MXR2MXF M) = 3 & len (MXR2MXF M) = 3 )
by MATRIX_0:24;
0. (F_Real,3,3) = (MXR2MXF M) * (0. (F_Real,3,3))
by Lm19;
hence 0_Rmatrix 3 =
MXF2MXR ((MXR2MXF M) * (0. (F_Real,3,3)))
by MATRIXR1:def 8
.=
(MXF2MXR (MXR2MXF M)) * (MXF2MXR (0. (F_Real,3,3)))
by Lm05
.=
M * (MXF2MXR (0. (F_Real,3,3)))
by Lm06
.=
M * (0_Rmatrix 3)
by MATRIXR1:def 8
;
(0_Rmatrix 3) * M = 0_Rmatrix 3
0. (F_Real,3,3) = (0. (F_Real,3,3)) * (MXR2MXF M)
by A1, MATRIX_5:22;
hence 0_Rmatrix 3 =
MXF2MXR ((0. (F_Real,3,3)) * (MXR2MXF M))
by MATRIXR1:def 8
.=
(MXF2MXR (0. (F_Real,3,3))) * (MXF2MXR (MXR2MXF M))
by Lm05
.=
(MXF2MXR (0. (F_Real,3,3))) * M
by Lm06
.=
(0_Rmatrix 3) * M
by MATRIXR1:def 8
;
verum