:: deftheorem Def2 defines continuous NFCONT_3:def 2 :
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f is continuous iff for x0 being Real st x0 in dom f holds
f is_continuous_in x0 );