let a, b, c be non zero Element of F_Real; :: thesis: <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> is invertible Matrix of 3,F_Real

reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;

reconsider M = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*>, N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> as Matrix of 3,F_Real by MATRIXR2:35;

reconsider ia = 1 / a, ib = 1 / b, ic = 1 / c as Element of F_Real by XREAL_0:def 1;

reconsider M = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*>, N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> as Matrix of 3,F_Real by MATRIXR2:35;

now :: thesis: ( N * M = 1. (F_Real,3) & N * M = M * N )

hence
<*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> is invertible Matrix of 3,F_Real
by MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verumthus
N * M = 1. (F_Real,3)
by Th09; :: thesis: N * M = M * N

hence N * M = M * N by Th09; :: thesis: verum

end;hence N * M = M * N by Th09; :: thesis: verum