:: deftheorem defines is_continuous_in PDIFF_7:def 6 :
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS n) st
( x0 = y0 & f = g & g is_continuous_in y0 ) );