let n be Element of NAT ; :: thesis: for x0 being Real
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; :: 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 A1: (dom f) /\ N = {x0} ; :: thesis: f is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
g is_continuous_in x0 by A1, NFCONT_3:11;
hence f is_continuous_in x0 ; :: thesis: verum