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 ;

_{1} being Matrix of 3,F_Real st b_{1} = a * N holds

b_{1} is invertible
by MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum

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) )

hence
for bA4:
( 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;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

b