theorem :: MATRIXR2:97

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 x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds
A is invertible