for n being Nat
for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) holds
ex B being Matrix of n,REAL st A * B = 1_Rmatrix n