0_Rmatrix 3 = MXF2MXR (0. (F_Real,3,3)) by MATRIXR1:def 8;
hence <*<*0,0,0*>,<*0,0,0*>,<*0,0,0*>*> = 0_Rmatrix 3 by MATRIXR1:def 2, Lm17; :: thesis: verum