:: deftheorem defines invertible MATRIXR2:def 5 :
for n being Nat
for A being Matrix of n,REAL holds
( A is invertible iff ex B being Matrix of n,REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) );