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) = () * (N2 * N) by XCMPLX_1:106
.= N2 * N by ;
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 ;
hence (b * N2) * (a * N) = b * (N2 * (a * N)) by MATRIX15:1
.= b * (a * (N2 * N)) by
.= (b * a) * (N2 * N) by MATRIX15:2
.= (a * b) * (N * N2) by
.= a * (b * (N * N2)) by MATRIX15:2
.= a * (N * (b * N2)) by
.= (a * N) * (b * N2) by ;
:: thesis: (b * N2) * (a * N) = 1. (F_Real,3)
thus (b * N2) * (a * N) = b * (N2 * (a * N)) by
.= b * (a * (N2 * N)) by
.= N2 * N by
.= 1. (F_Real,3) by ; :: thesis: verum
end;
hence for b1 being Matrix of 3,F_Real st b1 = a * N holds
b1 is invertible by ; :: thesis: verum