consider N2 being Matrix of 3,F_Real such that
A1: N is_reverse_of N2 by MATRIX_6:def 3;
reconsider b = 1 / a as Element of F_Real by XREAL_0:def 1;
A2: 1_ F_Real = 1. F_Real ;
not a is zero ;
then A3: (b * a) * (N2 * N) = (1. F_Real) * (N2 * N) by XCMPLX_1:106
.= N2 * N by A2, MATRIX15:2 ;

now :: thesis: ( (b * N2) * (a * N) = (a * N) * (b * N2) & (b * N2) * (a * N) = 1. (F_Real,3) )

A4: ( width N2 = 3 & width N = 3 ) by MATRIX_0:23;
then A5: ( width N2 = len N & width N = len N2 ) by MATRIX_0:23;
A6: ( width N2 = len (a * N) & width N = len (b * N2) ) by A4, MATRIX_0:23;
hence (b * N2) * (a * N) = b * (N2 * (a * N)) by MATRIX15:1
.= b * (a * (N2 * N)) by A5, MATRIXR1:22
.= (b * a) * (N2 * N) by MATRIX15:2
.= (a * b) * (N * N2) by A1, MATRIX_6:def 2
.= a * (b * (N * N2)) by MATRIX15:2
.= a * (N * (b * N2)) by A5, MATRIXR1:22
.= (a * N) * (b * N2) by A6, MATRIX15:1 ;
:: thesis: (b * N2) * (a * N) = 1. (F_Real,3)
thus (b * N2) * (a * N) = b * (N2 * (a * N)) by A6, MATRIX15:1
.= b * (a * (N2 * N)) by A5, MATRIXR1:22
.= N2 * N by A3, MATRIX15:2
.= 1. (F_Real,3) by A1, MATRIX_6:def 2 ; :: thesis: verum

end;

hence for b₁ being Matrix of 3,F_Real st b₁ = a * N holds
b₁ is invertible by MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum