let X, X1 be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of S,REAL st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let S be RealNormSpace; :: thesis: for f being PartFunc of S,REAL st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1
let f be PartFunc of S,REAL; :: thesis: ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 )
assume that
A1: f is_continuous_on X and
A2: X1 c= X ; :: thesis: f is_continuous_on X1
X c= dom f by A1;
hence A3: X1 c= dom f by A2; :: according to NFCONT_1:def 8 :: thesis: for b₁ being Element of the carrier of S holds
( not b₁ in X1 or f | X1 is_continuous_in b₁ )
let r be Point of S; :: thesis: ( not r in X1 or f | X1 is_continuous_in r )
assume A4: r in X1 ; :: thesis: f | X1 is_continuous_in r
then A5: f | X is_continuous_in r by A1, A2;
thus f | X1 is_continuous_in r :: thesis: verum

proof

(dom f) /\ X1 c= (dom f) /\ X by A2, XBOOLE_1:26;
then dom (f | X1) c= (dom f) /\ X by RELAT_1:61;
then A6: dom (f | X1) c= dom (f | X) by RELAT_1:61;
r in (dom f) /\ X1 by A3, A4, XBOOLE_0:def 4;
hence A7: r in dom (f | X1) by RELAT_1:61; :: according to NFCONT_1:def 6 :: thesis: for b₁ being Element of bool [:NAT, the carrier of S:] holds
( not rng b₁ c= dom (f | X1) or not b₁ is convergent or not lim b₁ = r or ( (f | X1) /* b₁ is convergent & (f | X1) /. r = lim ((f | X1) /* b₁) ) )
then A8: (f | X) /. r = f /. r by A6, PARTFUN2:15
.= (f | X1) /. r by A7, PARTFUN2:15 ;
let s1 be sequence of S; :: thesis: ( not rng s1 c= dom (f | X1) or not s1 is convergent or not lim s1 = r or ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) )
assume that
A9: rng s1 c= dom (f | X1) and
A10: ( s1 is convergent & lim s1 = r ) ; :: thesis: ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) )
A11: rng s1 c= dom (f | X) by A9, A6;

A12: now :: thesis: for n being Element of NAT holds ((f | X) /* s1) . n = ((f | X1) /* s1) . n

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n = ((f | X1) /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A13: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A9, A6, FUNCT_2:109, XBOOLE_1:1
.= f /. (s1 . n) by A9, A6, A13, PARTFUN2:15
.= (f | X1) /. (s1 . n) by A9, A13, PARTFUN2:15
.= ((f | X1) /* s1) . n by A9, FUNCT_2:109 ; :: thesis: verum

end;

( (f | X) /* s1 is convergent & (f | X) /. r = lim ((f | X) /* s1) ) by A5, A10, A11;
hence ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) by A8, A12, FUNCT_2:63; :: thesis: verum

end;