:: deftheorem defines is_continuous_in NFCONT_4:def 1 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being Real holds
( f is_continuous_in x0 iff ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 ) );