let X, Y be RealNormSpace; :: thesis: for f being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let f be Function of (TopSpaceNorm X),(TopSpaceNorm Y); :: thesis: for ft being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let ft be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); :: thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let x be Point of (TopSpaceNorm X); :: thesis: for xt being Point of (LinearTopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_at x iff ft is_continuous_at xt )
let xt be Point of (LinearTopSpaceNorm X); :: 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 (TopSpaceNorm Y) 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 A3, TMAP_1:def 2;
H is Subset of (LinearTopSpaceNorm X) by Def4;
then reconsider Ht = H as a_neighborhood of xt by A2, Th34;
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: f is_continuous_at x

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 (LinearTopSpaceNorm Y) 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 A5, TMAP_1:def 2;
Ht is Subset of (TopSpaceNorm X) by Def4;
then reconsider H = Ht as a_neighborhood of x by A2, Th34;
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