per cases
( f | X is empty or not f | X is empty )
;

end;

suppose
f | X is empty
; :: thesis: for b_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous

b

hence
for b_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous
; :: thesis: verum

end;b

suppose
not f | X is empty
; :: thesis: for b_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous

b

then consider x0 being Real such that

A1: x0 in dom (f | X) by MEMBERED:9;

x0 in X by A1, RELAT_1:57;

then A2: X = {x0} by ZFMISC_1:132;

_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous
; :: thesis: verum

end;A1: x0 in dom (f | X) by MEMBERED:9;

x0 in X by A1, RELAT_1:57;

then A2: X = {x0} by ZFMISC_1:132;

now :: thesis: for p being Real st p in dom (f | X) holds

f | X is_continuous_in p

hence
for bf | X is_continuous_in p

let p be Real; :: thesis: ( p in dom (f | X) implies f | X is_continuous_in p )

assume p in dom (f | X) ; :: thesis: f | X is_continuous_in p

then A3: p in {x0} by A2;

thus f | X is_continuous_in p :: thesis: verum

end;assume p in dom (f | X) ; :: thesis: f | X is_continuous_in p

then A3: p in {x0} by A2;

thus f | X is_continuous_in p :: thesis: verum

proof

let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = p implies ( (f | X) /* s1 is convergent & (f | X) . p = lim ((f | X) /* s1) ) )

assume that

A4: rng s1 c= dom (f | X) and

s1 is convergent and

lim s1 = p ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) . p = lim ((f | X) /* s1) )

A5: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;

rng s1 c= (dom f) /\ {x0} by A2, A4, RELAT_1:61;

then A6: rng s1 c= {x0} by A5;

hence (f | X) . p = lim ((f | X) /* s1) by A2, A9, SEQ_2:def 7; :: thesis: verum

end;assume that

A4: rng s1 c= dom (f | X) and

s1 is convergent and

lim s1 = p ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) . p = lim ((f | X) /* s1) )

A5: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;

rng s1 c= (dom f) /\ {x0} by A2, A4, RELAT_1:61;

then A6: rng s1 c= {x0} by A5;

A7: now :: thesis: for n being Element of NAT holds s1 . n = x0

A8:
p = x0
by A3, TARSKI:def 1;let n be Element of NAT ; :: thesis: s1 . n = x0

s1 . n in rng s1 by VALUED_0:28;

hence s1 . n = x0 by A6, TARSKI:def 1; :: thesis: verum

end;s1 . n in rng s1 by VALUED_0:28;

hence s1 . n = x0 by A6, TARSKI:def 1; :: thesis: verum

A9: now :: thesis: for g being Real st 0 < g holds

ex n being Nat st

for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

hence
(f | X) /* s1 is convergent
by A2, SEQ_2:def 6; :: thesis: (f | X) . p = lim ((f | X) /* s1)ex n being Nat st

for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st

for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g )

assume A10: 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

let m be Nat; :: thesis: ( n <= m implies |.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g )

assume n <= m ; :: thesis: |.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

A11: m in NAT by ORDINAL1:def 12;

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| = |.(((f | {x0}) . (s1 . m)) - ((f | {x0}) . x0)).| by A2, A8, A4, FUNCT_2:108, A11

.= |.(((f | {x0}) . x0) - ((f | {x0}) . x0)).| by A7, A11

.= 0 by ABSVALUE:2 ;

hence |.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g by A10; :: thesis: verum

end;for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g )

assume A10: 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

let m be Nat; :: thesis: ( n <= m implies |.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g )

assume n <= m ; :: thesis: |.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g

A11: m in NAT by ORDINAL1:def 12;

|.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| = |.(((f | {x0}) . (s1 . m)) - ((f | {x0}) . x0)).| by A2, A8, A4, FUNCT_2:108, A11

.= |.(((f | {x0}) . x0) - ((f | {x0}) . x0)).| by A7, A11

.= 0 by ABSVALUE:2 ;

hence |.((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)).| < g by A10; :: thesis: verum

hence (f | X) . p = lim ((f | X) /* s1) by A2, A9, SEQ_2:def 7; :: thesis: verum

b