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