let f be Function of R^1 ,R^1 ; :: thesis: for g being PartFunc of REAL ,REAL
for x being Point of R^1 st f = g & g is_continuous_in x holds
f is_continuous_at x
let g be PartFunc of REAL ,REAL ; :: thesis: for x being Point of R^1 st f = g & g is_continuous_in x holds
f is_continuous_at x
let x be Point of R^1 ; :: thesis: ( f = g & g is_continuous_in x implies f is_continuous_at x )
assume that
A1: f = g and
A2: g is_continuous_in x ; :: thesis: f is_continuous_at x
let G be a_neighborhood of f . x; :: according to TMAP_1:def 2 :: thesis: ex b₁ being a_neighborhood of x st f .: b₁ c= G
consider Z being Neighbourhood of g . x such that
A3: Z c= G by A1, Th41;
consider N being Neighbourhood of x such that
A4: g .: N c= Z by A2, FCONT_1:5;
reconsider H = N as a_neighborhood of x by Th40, TOPMETR:24;
take H ; :: thesis: f .: H c= G
thus f .: H c= G by A1, A3, A4, XBOOLE_1:1; :: thesis: verum