let X, Y be RealNormSpace; :: thesis: for f being Function of (),()
for ft being Function of ,
for x being Point of ()
for xt being Point of st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )

let f be Function of (),(); :: thesis: for ft being Function of ,
for x being Point of ()
for xt being Point of st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )

let ft be Function of ,; :: thesis: for x being Point of ()
for xt being Point of st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )

let x be Point of (); :: thesis: for xt being Point of st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )

let xt be Point of ; :: thesis: ( f = ft & x = xt implies ( f is_continuous_at x iff ft is_continuous_at xt ) )
assume that
A1: f = ft and
A2: x = xt ; :: thesis: ( f is_continuous_at x iff ft is_continuous_at xt )
hereby :: thesis: ( ft is_continuous_at xt implies f is_continuous_at x )
assume A3: f is_continuous_at x ; :: thesis: ft is_continuous_at xt
now :: thesis: for Gt being a_neighborhood of ft . xt ex Ht being a_neighborhood of xt st ft .: Ht c= Gt
let Gt be a_neighborhood of ft . xt; :: thesis: ex Ht being a_neighborhood of xt st ft .: Ht c= Gt
Gt is Subset of () by Def4;
then reconsider G = Gt as a_neighborhood of f . x by A1, A2, Th34;
consider H being a_neighborhood of x such that
A4: f .: H c= G by ;
H is Subset of by Def4;
then reconsider Ht = H as a_neighborhood of xt by ;
take Ht = Ht; :: thesis: ft .: Ht c= Gt
thus ft .: Ht c= Gt by A1, A4; :: thesis: verum
end;
hence ft is_continuous_at xt by TMAP_1:def 2; :: thesis: verum
end;
assume A5: ft is_continuous_at xt ; :: thesis:
now :: thesis: for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G
let G be a_neighborhood of f . x; :: thesis: ex H being a_neighborhood of x st f .: H c= G
G is Subset of by Def4;
then reconsider Gt = G as a_neighborhood of ft . xt by A1, A2, Th34;
consider Ht being a_neighborhood of xt such that
A6: ft .: Ht c= Gt by ;
Ht is Subset of () by Def4;
then reconsider H = Ht as a_neighborhood of x by ;
take H = H; :: thesis: f .: H c= G
thus f .: H c= G by A1, A6; :: thesis: verum
end;
hence f is_continuous_at x by TMAP_1:def 2; :: thesis: verum