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