theorem LM3C: :: DUALSP04:11

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_continuous_on the carrier of X iff g is_continuous_on the carrier of (RUSp2RNSp X) )