let N be invertible Matrix of 3,F_Real; :: thesis: for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
NR @ is invertible
let NR be Matrix of 3,REAL; :: thesis: ( NR = MXF2MXR N implies NR @ is invertible )
assume A1: NR = MXF2MXR N ; :: thesis: NR @ is invertible
reconsider C = (MXR2MXF (NR @)) ~ as Matrix of 3,F_Real ;
reconsider B = MXF2MXR ((MXR2MXF (NR @)) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
( (NR @) * B = 1_Rmatrix 3 & B * (NR @) = 1_Rmatrix 3 ) by A1, Lm11, Lm09;
hence NR @ is invertible ; :: thesis: verum