theorem Th9: :: LOPBAN15:7

ex f being LinearOperator of RNS_Real,(REAL-NS 1) st
( f is isomorphism & ( for x being Element of RNS_Real holds f . x = <*x*> ) )