theorem Th89: :: MATRIXR2:89

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) )