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 )

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 A5:
ft is_continuous_at xt
; :: thesis: f is_continuous_at xassume A3:
f is_continuous_at x
; :: thesis: ft is_continuous_at xt

end;now :: thesis: for Gt being a_neighborhood of ft . xt ex Ht being a_neighborhood of xt st ft .: Ht c= Gt

hence
ft is_continuous_at xt
by TMAP_1:def 2; :: thesis: verumlet 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;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

now :: thesis: for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G

hence
f is_continuous_at x
by TMAP_1:def 2; :: thesis: verumlet 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;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