let n be Nat; :: thesis: for N being invertible Matrix of n,F_Real
for M being Matrix of n,REAL st M = MXF2MXR N holds
M is invertible
let N be invertible Matrix of n,F_Real; :: thesis: for M being Matrix of n,REAL st M = MXF2MXR N holds
M is invertible
let M be Matrix of n,REAL; :: thesis: ( M = MXF2MXR N implies M is invertible )
assume A1: M = MXF2MXR N ; :: thesis: M is invertible
A2: N ~ is_reverse_of N by MATRIX_6:def 4;
reconsider M2 = MXF2MXR (N ~) as Matrix of n,REAL by MATRIXR1:def 2;

now :: thesis: ( M * M2 = 1_Rmatrix n & M2 * M = 1_Rmatrix n )

thus M * M2 = 1_Rmatrix n :: thesis: M2 * M = 1_Rmatrix n

proof

M * M2 = MXF2MXR (N * (N ~)) by A1, Lm05
.= 1_Rmatrix n by A2, MATRIX_6:def 2 ;
hence M * M2 = 1_Rmatrix n ; :: thesis: verum

end;

thus M2 * M = 1_Rmatrix n :: thesis: verum

proof

M2 * M = MXF2MXR ((N ~) * N) by A1, Lm05
.= 1_Rmatrix n by A2, MATRIX_6:def 2 ;
hence M2 * M = 1_Rmatrix n ; :: thesis: verum

end;

end;

hence M is invertible ; :: thesis: verum