let x0 be Complex; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st x0 in dom f holds
f is_continuous_on {x0}
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( x0 in dom f implies f is_continuous_on {x0} )
assume A1: x0 in dom f ; :: thesis: f is_continuous_on {x0}
thus {x0} c= dom f by A1, TARSKI:def 1; :: according to CFCONT_1:def 2 :: thesis: for x0 being Complex st x0 in {x0} holds
f | {x0} is_continuous_in x0
let t be Complex; :: thesis: ( t in {x0} implies f | {x0} is_continuous_in t )
assume A2: t in {x0} ; :: thesis: f | {x0} is_continuous_in t
thus f | {x0} is_continuous_in t :: thesis: verum

proof

t in dom f by A1, A2, TARSKI:def 1;
then t in (dom f) /\ {x0} by A2, XBOOLE_0:def 4;
hence t in dom (f | {x0}) by RELAT_1:61; :: according to CFCONT_1:def 1 :: thesis: for s1 being Complex_Sequence st rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = t holds
( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) )
let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = t implies ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) ) )
assume that
A3: rng s1 c= dom (f | {x0}) and
s1 is convergent and
lim s1 = t ; :: thesis: ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. t = lim ((f | {x0}) /* s1) )
A4: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= (dom f) /\ {x0} by A3, RELAT_1:61;
then A5: rng s1 c= {x0} by A4;

A6: 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 A5, TARSKI:def 1; :: thesis: verum

end;

A7: t = x0 by A2, TARSKI:def 1;

A8: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r )
assume A9: 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
let m be Nat; :: thesis: ( n <= m implies |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r )
assume n <= m ; :: thesis: |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
A10: m in NAT by ORDINAL1:def 12;
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| = |.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).| by A7, A3, FUNCT_2:109, A10
.= |.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).| by A6
.= 0 by COMPLEX1:44 ;
hence |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r by A9; :: thesis: verum

end;

hence (f | {x0}) /* s1 is convergent ; :: thesis: (f | {x0}) /. t = lim ((f | {x0}) /* s1)
hence (f | {x0}) /. t = lim ((f | {x0}) /* s1) by A8, COMSEQ_2:def 6; :: thesis: verum

end;