consider I being LinearOperator of RNS_Real,(REAL-NS 1) such that
A1: I is isomorphism by Th9;
consider K being Lipschitzian LinearOperator of (REAL-NS 1),RNS_Real such that
A2: ( K = I " & K is isomorphism ) by A1, NORMSP_3:37;
( REAL-NS 1 is finite-dimensional & dim (REAL-NS 1) = 1 ) by REAL_NS2:62;
hence ( RNS_Real is finite-dimensional & dim RNS_Real = 1 ) by A2, REAL_NS2:88; :: thesis: verum