let X be set ; :: thesis: for x0 being real number
for f being PartFunc of REAL ,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let x0 be real number ; :: thesis: for f being PartFunc of REAL ,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
let f be PartFunc of REAL ,REAL ; :: thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
Z: x0 in X and
Z0: f is_continuous_in x0 ; :: thesis: f | X is_continuous_in x0
let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: 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
Z1: rng s1 c= dom (f | X) and
Z2: s1 is convergent and
Z3: lim s1 = x0 ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) . x0 = lim ((f | X) /* s1) )
dom (f | X) = X /\ (dom f) by RELAT_1:90;
then A: rng s1 c= dom f by Z1, XBOOLE_1:18;
B: (f | X) /* s1 = f /* s1 by Z1, FUNCT_2:194;
hence (f | X) /* s1 is convergent by Z2, Def1, A, Z0, Z3; :: thesis: (f | X) . x0 = lim ((f | X) /* s1)
thus (f | X) . x0 = f . x0 by Z, FUNCT_1:72
.= lim ((f | X) /* s1) by B, Z2, Def1, A, Z0, Z3 ; :: thesis: verum