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