let X be set ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX st f is_continuous_on X & f " {0 } = {} holds
f ^ is_continuous_on X
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f is_continuous_on X & f " {0 } = {} implies f ^ is_continuous_on X )
assume that
A1: f is_continuous_on X and
A2: f " {0 } = {} ; :: thesis: f ^ is_continuous_on X
A3: dom (f ^ ) = (dom f) \ {} by A2, CFUNCT_1:def 2
.= dom f ;
hence A4: X c= dom (f ^ ) by A1, Def5; :: according to CFCONT_1:def 5 :: thesis: for x0 being Element of COMPLEX st x0 in X holds
(f ^ ) | X is_continuous_in x0
let g be Element of COMPLEX ; :: thesis: ( g in X implies (f ^ ) | X is_continuous_in g )
assume A5: g in X ; :: thesis: (f ^ ) | X is_continuous_in g
then A6: f | X is_continuous_in g by A1, Def5;
g in (dom (f ^ )) /\ X by A4, A5, XBOOLE_0:def 4;
then A7: g in dom ((f ^ ) | X) by RELAT_1:90;

now

let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom ((f ^ ) | X) & s1 is convergent & lim s1 = g implies ( ((f ^ ) | X) /* s1 is convergent & lim (((f ^ ) | X) /* s1) = ((f ^ ) | X) /. g ) )
assume A8: ( rng s1 c= dom ((f ^ ) | X) & s1 is convergent & lim s1 = g ) ; :: thesis: ( ((f ^ ) | X) /* s1 is convergent & lim (((f ^ ) | X) /* s1) = ((f ^ ) | X) /. g )
then rng s1 c= (dom (f ^ )) /\ X by RELAT_1:90;
then A9: rng s1 c= dom (f | X) by A3, RELAT_1:90;
then A10: ( (f | X) /* s1 is convergent & (f | X) /. g = lim ((f | X) /* s1) ) by A6, A8, Def2;
g in (dom f) /\ X by A3, A4, A5, XBOOLE_0:def 4;
then A11: g in dom (f | X) by RELAT_1:90;
then A12: (f | X) /. g = f /. g by PARTFUN2:32;

A13: now

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n <> 0c
A14: rng s1 c= (dom f) /\ X by A3, A8, RELAT_1:90;
(dom f) /\ X c= dom f by XBOOLE_1:17;
then A15: rng s1 c= dom f by A14, XBOOLE_1:1;
A16: s1 . n in rng s1 by VALUED_0:28;

A17: now

assume f /. (s1 . n) = 0c ; :: thesis: contradiction
then f /. (s1 . n) in {0c } by TARSKI:def 1;
hence contradiction by A2, A15, A16, PARTFUN2:44; :: thesis: verum

end;

((f | X) /* s1) . n = (f | X) /. (s1 . n) by A9, FUNCT_2:186
.= f /. (s1 . n) by A9, A16, PARTFUN2:32 ;
hence ((f | X) /* s1) . n <> 0c by A17; :: thesis: verum

end;

now

assume f /. g = 0c ; :: thesis: contradiction
then f /. g in {0c } by TARSKI:def 1;
hence contradiction by A2, A3, A4, A5, PARTFUN2:44; :: thesis: verum

end;

then A18: ( lim ((f | X) /* s1) <> 0c & (f | X) /* s1 is non-zero ) by A6, A8, A9, A12, A13, Def2, COMSEQ_1:4;

now

let n be Element of NAT ; :: thesis: (((f ^ ) | X) /* s1) . n = (((f | X) /* s1) " ) . n
A19: s1 . n in rng s1 by VALUED_0:28;
then s1 . n in dom ((f ^ ) | X) by A8;
then s1 . n in (dom (f ^ )) /\ X by RELAT_1:90;
then A20: s1 . n in dom (f ^ ) by XBOOLE_0:def 4;
thus (((f ^ ) | X) /* s1) . n = ((f ^ ) | X) /. (s1 . n) by A8, FUNCT_2:186
.= (f ^ ) /. (s1 . n) by A8, A19, PARTFUN2:32
.= (f /. (s1 . n)) " by A20, CFUNCT_1:def 2
.= ((f | X) /. (s1 . n)) " by A9, A19, PARTFUN2:32
.= (((f | X) /* s1) . n) " by A9, FUNCT_2:186
.= (((f | X) /* s1) " ) . n by VALUED_1:10 ; :: thesis: verum

end;

then A21: ((f ^ ) | X) /* s1 = ((f | X) /* s1) " by FUNCT_2:113;
hence ((f ^ ) | X) /* s1 is convergent by A10, A18, COMSEQ_2:34; :: thesis: lim (((f ^ ) | X) /* s1) = ((f ^ ) | X) /. g
thus lim (((f ^ ) | X) /* s1) = ((f | X) /. g) " by A10, A18, A21, COMSEQ_2:35
.= (f /. g) " by A11, PARTFUN2:32
.= (f ^ ) /. g by A4, A5, CFUNCT_1:def 2
.= ((f ^ ) | X) /. g by A7, PARTFUN2:32 ; :: thesis: verum

end;

hence (f ^ ) | X is_continuous_in g by A7, Def2; :: thesis: verum