let X, Y be RealNormSpace; :: thesis: for f being PartFunc of X,Y
for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y) st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )
let f be PartFunc of X,Y; :: thesis: for ft being Function of (TopSpaceNorm X),(TopSpaceNorm Y) st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )
let ft be Function of (TopSpaceNorm X),(TopSpaceNorm Y); :: thesis: ( f = ft implies ( f is_continuous_on the carrier of X iff ft is continuous ) )
assume A1: f = ft ; :: thesis: ( f is_continuous_on the carrier of X iff ft is continuous )
then A2: dom f = the carrier of X by FUNCT_2:def 1;
A3: f | the carrier of X = f by RELSET_1:34;

hereby :: thesis: ( ft is continuous implies f is_continuous_on the carrier of X )

assume A4: f is_continuous_on the carrier of X ; :: thesis: ft is continuous

now

let xt be Point of (TopSpaceNorm X); :: thesis: ft is_continuous_at xt
reconsider x = xt as Point of X ;
f | the carrier of X is_continuous_in x by A4, NFCONT_1:def 11;
hence ft is_continuous_at xt by A1, A3, Th18; :: thesis: verum

end;

hence ft is continuous by TMAP_1:49; :: thesis: verum

end;

assume A5: ft is continuous ; :: thesis: f is_continuous_on the carrier of X

now

let x be Point of X; :: thesis: ( x in the carrier of X implies f | the carrier of X is_continuous_in x )
assume x in the carrier of X ; :: thesis: f | the carrier of X is_continuous_in x
reconsider xt = x as Point of (TopSpaceNorm X) ;
ft is_continuous_at xt by A5, TMAP_1:49;
hence f | the carrier of X is_continuous_in x by A1, A3, Th18; :: thesis: verum

end;

hence f is_continuous_on the carrier of X by A2, NFCONT_1:def 11; :: thesis: verum