let x0 be Real; :: thesis: for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

let f be PartFunc of REAL, the carrier of S; :: 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

x0 in (dom f) /\ N by A1, TARSKI:def 1;

then A2: x0 in dom f by XBOOLE_0:def 4;

for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

let f be PartFunc of REAL, the carrier of S; :: 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

x0 in (dom f) /\ N by A1, TARSKI:def 1;

then A2: x0 in dom f by XBOOLE_0:def 4;

now :: thesis: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1

hence
f is_continuous_in x0
by Th10, A2; :: thesis: verumlet N1 be Neighbourhood of f /. x0; :: thesis: ex N being Neighbourhood of x0 st f .: N c= N1

take N = N; :: thesis: f .: N c= N1

A3: f /. x0 in N1 by NFCONT_1:4;

f .: N = Im (f,x0) by A1, RELAT_1:112

.= {(f . x0)} by A2, FUNCT_1:59

.= {(f /. x0)} by A2, PARTFUN1:def 6 ;

hence f .: N c= N1 by A3, ZFMISC_1:31; :: thesis: verum

end;take N = N; :: thesis: f .: N c= N1

A3: f /. x0 in N1 by NFCONT_1:4;

f .: N = Im (f,x0) by A1, RELAT_1:112

.= {(f . x0)} by A2, FUNCT_1:59

.= {(f /. x0)} by A2, PARTFUN1:def 6 ;

hence f .: N c= N1 by A3, ZFMISC_1:31; :: thesis: verum