for n being Nat
for A being Matrix of n,REAL st A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )