for n being Nat
for N being Matrix of n,REAL st N is invertible holds
( N @ is invertible & Inv (N @) = (Inv N) @ )