theorem Th93: :: MATRIXR2:93

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