let n be Nat; :: thesis: for M being Matrix of n,REAL
for N being Matrix of n,F_Real st M = N holds
( M is invertible iff N is invertible )
let M be Matrix of n,REAL; :: thesis: for N being Matrix of n,F_Real st M = N holds
( M is invertible iff N is invertible )
let N be Matrix of n,F_Real; :: thesis: ( M = N implies ( M is invertible iff N is invertible ) )
assume A1: M = N ; :: thesis: ( M is invertible iff N is invertible )
A2: 1. (F_Real,n) = MXF2MXR (1. (F_Real,n)) by MATRIXR1:def 2
.= 1_Rmatrix n by MATRIXR2:def 2 ;

hereby :: thesis: ( N is invertible implies M is invertible )

assume M is invertible ; :: thesis: N is invertible
then consider B being Matrix of n,REAL such that
A3: B * M = 1_Rmatrix n and
A4: M * B = 1_Rmatrix n by MATRIXR2:def 5;
reconsider C = B as Matrix of n,F_Real ;
A5: B * M = C * N by A1, Th15;
C is_reverse_of N

proof

C * N = N * C by A1, A3, A4, A5, Th15;
hence C is_reverse_of N by A2, A3, A1, Th15, MATRIX_6:def 2; :: thesis: verum

end;

hence N is invertible by MATRIX_6:def 3; :: thesis: verum

end;

assume N is invertible ; :: thesis: M is invertible
then consider N2 being Matrix of n,F_Real such that
A6: N is_reverse_of N2 by MATRIX_6:def 3;
reconsider M2 = N2 as Matrix of n,REAL ;

now :: thesis: ex M2 being Matrix of n,REAL st
( M2 * M = 1_Rmatrix n & M * M2 = 1_Rmatrix n )

take M2 = M2; :: thesis: ( M2 * M = 1_Rmatrix n & M * M2 = 1_Rmatrix n )
A7: M2 * M = N2 * N by A1, Th15
.= 1. (F_Real,n) by A6, MATRIX_6:def 2 ;
hence M2 * M = 1_Rmatrix n by A2; :: thesis: M * M2 = 1_Rmatrix n
M2 * M = N2 * N by A1, Th15
.= N * N2 by A6, MATRIX_6:def 2
.= M * M2 by A1, Th15 ;
hence M * M2 = 1_Rmatrix n by A7, A2; :: thesis: verum

end;

hence M is invertible by MATRIXR2:def 5; :: thesis: verum