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 )
A2: f | the carrier of X = f by RELSET_1:19;

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

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

now :: thesis: for xt being Point of (TopSpaceNorm X) holds ft is_continuous_at xt

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 A3, NFCONT_1:def 7;
hence ft is_continuous_at xt by A1, A2, Th18; :: thesis: verum

end;

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

end;

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

A5: now :: thesis: for x being Point of X st x in the carrier of X holds
f | the carrier of X is_continuous_in x

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 A4, TMAP_1:44;
hence f | the carrier of X is_continuous_in x by A1, A2, Th18; :: thesis: verum

end;

dom f = the carrier of X by A1, FUNCT_2:def 1;
hence f is_continuous_on the carrier of X by A5, NFCONT_1:def 7; :: thesis: verum