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;

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

thus N * M = 1. (F_Real,3) by Th09; :: thesis: N * M = M * N
hence N * M = M * N by Th09; :: thesis: verum

end;

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: verum