let X be set ; :: thesis: 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; :: 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

A1: x0 in X and

A2: 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

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) )

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; :: thesis: (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 ; :: thesis: verum

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; :: 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

A1: x0 in X and

A2: 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

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) )

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; :: thesis: (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 ; :: thesis: verum