let x0 be Element of 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 :: according to CFCONT_1:def 2 :: thesis: for x0 being Element of COMPLEX st x0 in {x0} holds
f | {x0} is_continuous_in x0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in dom f )
assume x in {x0} ; :: thesis: x in dom f
hence x in dom f by A1, TARSKI:def 1; :: thesis: verum

end;

let t be Element of 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, XBOOLE_1:1;

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

end;

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

A8: now

let r be Real; :: thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r )
assume A9: 0 < r ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r
let m be Element of 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
|.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| = |.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).| by A7, A3, FUNCT_2:109
.= |.(((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 by COMSEQ_2:def 4; :: thesis: (f | {x0}) /. t = lim ((f | {x0}) /* s1)
hence (f | {x0}) /. t = lim ((f | {x0}) /* s1) by A8, COMSEQ_2:def 5; :: thesis: verum

end;