let X be set ; :: thesis: for S, T being RealNormSpace
for f being PartFunc of S,T holds
( f is_continuous_on X iff f | X is_continuous_on X )
let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T holds
( f is_continuous_on X iff f | X is_continuous_on X )
let f be PartFunc of S,T; :: thesis: ( f is_continuous_on X iff f | X is_continuous_on X )
thus ( f is_continuous_on X implies f | X is_continuous_on X ) :: thesis: ( f | X is_continuous_on X implies f is_continuous_on X )

proof

assume A1: f is_continuous_on X ; :: thesis: f | X is_continuous_on X
then X c= dom f ;
then X c= (dom f) /\ X by XBOOLE_1:28;
hence X c= dom (f | X) by RELAT_1:61; :: according to NFCONT_1:def 7 :: thesis: for x0 being Point of S st x0 in X holds
(f | X) | X is_continuous_in x0
let r be Point of S; :: thesis: ( r in X implies (f | X) | X is_continuous_in r )
assume r in X ; :: thesis: (f | X) | X is_continuous_in r
then f | X is_continuous_in r by A1;
hence (f | X) | X is_continuous_in r by RELAT_1:72; :: thesis: verum

end;

assume A2: f | X is_continuous_on X ; :: thesis: f is_continuous_on X
then X c= dom (f | X) ;
then ( (dom f) /\ X c= dom f & X c= (dom f) /\ X ) by RELAT_1:61, XBOOLE_1:17;
hence X c= dom f ; :: according to NFCONT_1:def 7 :: thesis: for x0 being Point of S st x0 in X holds
f | X is_continuous_in x0
let r be Point of S; :: thesis: ( r in X implies f | X is_continuous_in r )
assume r in X ; :: thesis: f | X is_continuous_in r
then (f | X) | X is_continuous_in r by A2;
hence f | X is_continuous_in r by RELAT_1:72; :: thesis: verum