let X be set ; :: thesis: for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let x0 be real number ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let f be PartFunc of REAL, the carrier of S; :: thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
A1: x0 in X and
A2: f is_continuous_in x0 ; :: thesis: f | X is_continuous_in x0
A0: x0 in dom f by Def1, A2;
X0: dom (f | X) = X /\ (dom f) by RELAT_1:90;
hence X1: x0 in dom (f | X) by A1, A0, XBOOLE_0:def 4; :: according to NFCONT_3:def 1 :: thesis: for s1 being Real_Sequence st rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x0 holds
( (f | X) /* s1 is convergent & (f | X) /. x0 = lim ((f | X) /* s1) )
let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x0 implies ( (f | X) /* s1 is convergent & (f | X) /. x0 = lim ((f | X) /* s1) ) )
assume that
A3: rng s1 c= dom (f | X) and
A4: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) /. x0 = lim ((f | X) /* s1) )
A5: rng s1 c= dom f by A3, XBOOLE_1:18, X0;
A6: (f | X) /* s1 = f /* s1 by A3, FUNCT_2:194;
hence (f | X) /* s1 is convergent by A2, A4, A5, Def1; :: thesis: (f | X) /. x0 = lim ((f | X) /* s1)
thus (f | X) /. x0 = f /. x0 by X1, PARTFUN2:32
.= lim ((f | X) /* s1) by A2, A4, A5, A6, Def1 ; :: thesis: verum