let X, Y be RealNormSpace; :: thesis: for f being PartFunc of X,Y
for ft being Function of (),() 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 (),() st f = ft holds
( f is_continuous_on the carrier of X iff ft is continuous )

let ft be Function of (),(); :: 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 () holds ft is_continuous_at xt
let xt be Point of (); :: thesis: ft is_continuous_at xt
reconsider x = xt as Point of X ;
f | the carrier of X is_continuous_in x by ;
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 () ;
ft is_continuous_at xt by ;
hence f | the carrier of X is_continuous_in x by A1, A2, Th18; :: thesis: verum
end;
dom f = the carrier of X by ;
hence f is_continuous_on the carrier of X by ; :: thesis: verum