let X be set ; for x0 being Real
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; 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; ( 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
; f | X is_continuous_in x0
let s1 be Real_Sequence; FCONT_1:def 1 ( 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 )
; ( (f | X) /* s1 is convergent & (f | X) . x0 = lim ((f | X) /* s1) )
dom (f | X) = X /\ (dom f)
by RELAT_1:61;
then A5:
rng s1 c= dom f
by A3, XBOOLE_1:18;
A6:
(f | X) /* s1 = f /* s1
by A3, FUNCT_2:117;
hence
(f | X) /* s1 is convergent
by A2, A4, A5; (f | X) . x0 = lim ((f | X) /* s1)
thus (f | X) . x0 =
f . x0
by A1, FUNCT_1:49
.=
lim ((f | X) /* s1)
by A2, A4, A5, A6
; verum