theorem LM3B: :: DUALSP04:10

for X being RealUnitarySpace
for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),REAL
for x0 being Point of X
for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds
( f is_continuous_in x0 iff g is_continuous_in y0 )