let M be Matrix of 3,REAL; :: thesis: ( 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 ;
:: thesis: (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 ;
:: thesis: verum