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 A1: ( f = ft & x = xt ) ; :: thesis: ( f is_continuous_in x iff ft is_continuous_at xt )
then A2: dom f = the carrier of X by FUNCT_2:def 1;
then A3: ft . xt = f /. x by A1, PARTFUN1:def 8;

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

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

now

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 A3, Th17;
then consider N being Neighbourhood of x such that
A5: f .: N c= N1 by A4, NFCONT_1:17;
reconsider H = N as a_neighborhood of xt by A1, Th17;
take H = H; :: thesis: ft .: H c= G
thus ft .: H c= G by A1, A5; :: thesis: verum

end;

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

end;

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

now

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 A3, Th17;
then consider H being a_neighborhood of xt such that
A7: ft .: H c= G by A6, TMAP_1:def 2;
reconsider N = H as Subset of X ;
reconsider N = N as Neighbourhood of x by A1, Th17;
take N = N; :: thesis: f .: N c= N1
thus f .: N c= N1 by A1, A7; :: thesis: verum

end;

hence f is_continuous_in x by A2, NFCONT_1:17; :: thesis: verum