let n be Nat; :: thesis: for N being Matrix of n,REAL st N is invertible holds
( N @ is invertible & Inv (N @) = (Inv N) @ )
let N be Matrix of n,REAL; :: thesis: ( N is invertible implies ( N @ is invertible & Inv (N @) = (Inv N) @ ) )
assume A1: N is invertible ; :: thesis: ( N @ is invertible & Inv (N @) = (Inv N) @ )
then (N * (Inv N)) @ = (1_Rmatrix n) @ by MATRIXR2:def 6
.= 1_Rmatrix n by MATRIXR2:64 ;
then A2: ((Inv N) @) * (N @) = 1_Rmatrix n by MATRIXR2:30;
((Inv N) * N) @ = (1_Rmatrix n) @ by A1, MATRIXR2:def 6
.= 1_Rmatrix n by MATRIXR2:64 ;
then A3: (N @) * ((Inv N) @) = 1_Rmatrix n by MATRIXR2:30;
then N @ is invertible by A2, MATRIXR2:def 5;
hence ( N @ is invertible & Inv (N @) = (Inv N) @ ) by A2, A3, MATRIXR2:def 6; :: thesis: verum