now :: thesis: ( not f | X is empty implies for b₁ being PartFunc of REAL, the carrier of S st b₁ = f | X holds
b₁ is continuous )

assume not f | X is empty ; :: thesis: for b₁ being PartFunc of REAL, the carrier of S st b₁ = f | X holds
b₁ is continuous
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;

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

let p be Real; :: thesis: ( p in dom (f | X) implies f | X is_continuous_in p )
assume A3: p in dom (f | X) ; :: thesis: f | X is_continuous_in p
then A4: p in {x0} by A2;
thus f | X is_continuous_in p :: thesis: verum

proof

thus p in dom (f | X) by A3; :: according to NFCONT_3:def 1 :: thesis: for s1 being Real_Sequence st rng s1 c= dom (f | X) & s1 is convergent & lim s1 = p holds
( (f | X) /* s1 is convergent & (f | X) /. p = lim ((f | X) /* s1) )
let s1 be Real_Sequence; :: 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
A5: 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) )
A6: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= (dom f) /\ {x0} by A2, A5, RELAT_1:61;
then A7: rng s1 c= {x0} by A6, XBOOLE_1:1;

A8: now :: thesis: for n being Nat holds s1 . n = x0

let n be Nat; :: thesis: s1 . n = x0
s1 . n in rng s1 by VALUED_0:28;
hence s1 . n = x0 by A7, TARSKI:def 1; :: thesis: verum

end;

A9: p = x0 by A4, TARSKI:def 1;

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

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 A11: 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
A12: m in NAT by ORDINAL1:def 12;
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| = ||.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).|| by A2, A9, A5, FUNCT_2:109, A12
.= ||.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).|| by A8
.= 0 by NORMSP_1:6 ;
hence ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g by A11; :: thesis: verum

end;

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

end;

end;

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

end;

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