let n be Element of NAT ; :: thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let x0 be real number ; :: thesis: for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); :: thesis: ( ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 )
given N being Neighbourhood of x0 such that P1: (dom f) /\ N = {x0} ; :: thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
g is_continuous_in x0 by P1, NFCONT_3:11;
hence f is_continuous_in x0 by Def1Th; :: thesis: verum