:: deftheorem Def6 defines Inv MATRIXR2:def 6 :
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
for b₃ being Matrix of n,REAL holds
( b₃ = Inv A iff ( b₃ * A = 1_Rmatrix n & A * b₃ = 1_Rmatrix n ) );