theorem LMN7: :: DUALSP02:13

for X being RealNormSpace
for x being object holds
( x is additive homogeneous Lipschitzian Function of X,REAL iff x is additive homogeneous Lipschitzian Function of X,RNS_Real )