let X, Y be RealNormSpace; :: thesis: for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let f be PartFunc of X,Y; :: thesis: for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y)
for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let ft be Function of (TopSpaceNorm X),(TopSpaceNorm Y); :: thesis: for x being Point of X
for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let x be Point of X; :: thesis: for xt being Point of (TopSpaceNorm X) st f = ft & x = xt holds
( f is_continuous_in x iff ft is_continuous_at xt )
let xt be Point of (TopSpaceNorm X); :: thesis: ( f = ft & x = xt implies ( f is_continuous_in x iff ft is_continuous_at xt ) )
assume that
A1: f = ft and
A2: x = xt ; :: thesis: ( f is_continuous_in x iff ft is_continuous_at xt )
A3: dom f = the carrier of X by A1, FUNCT_2:def 1;
then A4: ft . xt = f /. x by A1, A2, PARTFUN1:def 6;

hereby :: thesis: ( ft is_continuous_at xt implies f is_continuous_in x )

assume A5: f is_continuous_in x ; :: thesis: ft is_continuous_at xt

now :: thesis: for G being a_neighborhood of ft . xt ex H being a_neighborhood of xt st ft .: H c= G

let G be a_neighborhood of ft . xt; :: thesis: ex H being a_neighborhood of xt st ft .: H c= G
reconsider N1 = G as Subset of Y ;
N1 is Neighbourhood of f /. x by A4, Th17;
then consider N being Neighbourhood of x such that
A6: f .: N c= N1 by A5, NFCONT_1:10;
reconsider H = N as a_neighborhood of xt by A2, Th17;
take H = H; :: thesis: ft .: H c= G
thus ft .: H c= G by A1, A6; :: thesis: verum

end;

hence ft is_continuous_at xt by TMAP_1:def 2; :: thesis: verum

end;

assume A7: ft is_continuous_at xt ; :: thesis: f is_continuous_in x

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

let N1 be Neighbourhood of f /. x; :: thesis: ex N being Neighbourhood of x st f .: N c= N1
reconsider G = N1 as Subset of Y ;
G is a_neighborhood of ft . xt by A4, Th17;
then consider H being a_neighborhood of xt such that
A8: ft .: H c= G by A7, TMAP_1:def 2;
reconsider N = H as Subset of X ;
reconsider N = N as Neighbourhood of x by A2, Th17;
take N = N; :: thesis: f .: N c= N1
thus f .: N c= N1 by A1, A8; :: thesis: verum

end;

hence f is_continuous_in x by A3, NFCONT_1:10; :: thesis: verum