theorem Th23: :: REAL_NS3:22

for V being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp V st dim V <> 0 holds
ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & ( for x being Element of (RLSp2RVSp V) holds S . x = x |-- b ) )