theorem LM4: :: DUALSP04:13

for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),REAL st f = g holds
( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )