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;

hence f is_continuous_on the carrier of X by A5, NFCONT_1:def 7; :: thesis: verum

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 A4:
ft is continuous
; :: thesis: f is_continuous_on the carrier of Xassume A3:
f is_continuous_on the carrier of X
; :: thesis: ft is continuous

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

hence
ft is continuous
by TMAP_1:44; :: thesis: verumlet 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;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

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

dom f = the carrier of X
by A1, FUNCT_2:def 1;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;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

hence f is_continuous_on the carrier of X by A5, NFCONT_1:def 7; :: thesis: verum