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

suppose f | X is empty ; :: thesis: for b₁ being PartFunc of REAL ,REAL st b₁ = f | X holds
b₁ is continuous

hence for b₁ being PartFunc of REAL ,REAL st b₁ = f | X holds
b₁ is continuous ; :: thesis: verum

end;

suppose not f | X is empty ; :: thesis: for b₁ being PartFunc of REAL ,REAL st b₁ = f | X holds
b₁ is continuous

then consider x0 being real number such that
W1: x0 in dom (f | X) by MEMBERED:9;
x0 in X by W1, RELAT_1:86;
then W: X = {x0} by REALSET1:17;

now

let p be real number ; :: 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 B2: p in {x0} by W, RELAT_1:86;
thus f | X is_continuous_in p :: thesis: verum

proof

A3: p = x0 by B2, TARSKI:def 1;
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 A4: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = p ) ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) . p = lim ((f | X) /* s1) )
then A5: rng s1 c= (dom f) /\ {x0} by W, RELAT_1:90;
(dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
then A6: rng s1 c= {x0} by A5, XBOOLE_1:1;

A7: now

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;

A8: now

let g be real number ; :: thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g )
assume A9: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g )
assume n <= m ; :: thesis: abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g
abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) = abs (((f | {x0}) . (s1 . m)) - ((f | {x0}) . x0)) by A3, A4, W, FUNCT_2:185
.= abs (((f | {x0}) . x0) - ((f | {x0}) . x0)) by A7
.= 0 by ABSVALUE:7 ;
hence abs ((((f | {x0}) /* s1) . m) - ((f | {x0}) . p)) < g by A9; :: thesis: verum

end;

hence (f | X) /* s1 is convergent by W, SEQ_2:def 6; :: thesis: (f | X) . p = lim ((f | X) /* s1)
hence (f | X) . p = lim ((f | X) /* s1) by A8, W, SEQ_2:def 7; :: thesis: verum

end;

end;

hence for b₁ being PartFunc of REAL ,REAL st b₁ = f | X holds
b₁ is continuous by Def2; :: thesis: verum

end;

end;