let n be Nat; :: thesis: for A being Matrix of n,REAL st A is invertible holds
Det (Inv A) = (Det A) "
let A be Matrix of n,REAL; :: thesis: ( A is invertible implies Det (Inv A) = (Det A) " )
assume A is invertible ; :: thesis: Det (Inv A) = (Det A) "
then A * (Inv A) = 1_Rmatrix n by Def6;
then Det (A * (Inv A)) = 1 by Th72;
then A1: (Det A) * (Det (Inv A)) = 1 by Th46;

per cases ( Det A <> 0 or Det A = 0 ) ;

suppose Det A <> 0 ; :: thesis: Det (Inv A) = (Det A) "

hence Det (Inv A) = (Det A) " by A1, XCMPLX_0:def 7; :: thesis: verum

end;

suppose Det A = 0 ; :: thesis: Det (Inv A) = (Det A) "

hence Det (Inv A) = (Det A) " by A1; :: thesis: verum

end;

end;