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