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; :: according to CFCONT_1:def 2 :: thesis: for x0 being Complex st x0 in X holds
(f ^) | X is_continuous_in x0
let g be 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;
g in (dom (f ^)) /\ X by A4, A5, XBOOLE_0:def 4;
then A7: g in dom ((f ^) | X) by RELAT_1:61;
now :: thesis: for s1 being Complex_Sequence st rng s1 c= dom ((f ^) | X) & s1 is convergent & lim s1 = g holds
( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) /. g )
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 that
A8: rng s1 c= dom ((f ^) | X) and
A9: ( s1 is convergent & lim s1 = g ) ; :: thesis: ( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) /. g )
rng s1 c= (dom (f ^)) /\ X by A8, RELAT_1:61;
then A10: rng s1 c= dom (f | X) by A3, RELAT_1:61;
then A11: (f | X) /* s1 is convergent by A6, A9;
now :: thesis: for n being Element of NAT holds ((f | X) /* s1) . n <> 0c
let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n <> 0c
A12: s1 . n in rng s1 by VALUED_0:28;
( rng s1 c= (dom f) /\ X & (dom f) /\ X c= dom f ) by A3, A8, RELAT_1:61, XBOOLE_1:17;
then A13: rng s1 c= dom f ;
A14: now :: thesis: not f /. (s1 . n) = 0c
assume f /. (s1 . n) = 0c ; :: thesis: contradiction
then f /. (s1 . n) in {0c} by TARSKI:def 1;
hence contradiction by A2, A13, A12, PARTFUN2:26; :: thesis: verum
end;
((f | X) /* s1) . n = (f | X) /. (s1 . n) by A10, FUNCT_2:109
.= f /. (s1 . n) by A10, A12, PARTFUN2:15 ;
hence ((f | X) /* s1) . n <> 0c by A14; :: thesis: verum
end;
then A15: (f | X) /* s1 is non-zero by COMSEQ_1:4;
g in (dom f) /\ X by A3, A4, A5, XBOOLE_0:def 4;
then A16: g in dom (f | X) by RELAT_1:61;
then A17: (f | X) /. g = f /. g by PARTFUN2:15;
now :: thesis: for n being Element of NAT holds (((f ^) | X) /* s1) . n = (((f | X) /* s1) ") . n
let n be Element of NAT ; :: thesis: (((f ^) | X) /* s1) . n = (((f | X) /* s1) ") . n
A18: 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:61;
then A19: s1 . n in dom (f ^) by XBOOLE_0:def 4;
thus (((f ^) | X) /* s1) . n = ((f ^) | X) /. (s1 . n) by A8, FUNCT_2:109
.= (f ^) /. (s1 . n) by A8, A18, PARTFUN2:15
.= (f /. (s1 . n)) " by A19, CFUNCT_1:def 2
.= ((f | X) /. (s1 . n)) " by A10, A18, PARTFUN2:15
.= (((f | X) /* s1) . n) " by A10, FUNCT_2:109
.= (((f | X) /* s1) ") . n by VALUED_1:10 ; :: thesis: verum
end;
then A20: ((f ^) | X) /* s1 = ((f | X) /* s1) " by FUNCT_2:63;
reconsider gg = g as Element of COMPLEX by XCMPLX_0:def 2;
A21: now :: thesis: not f /. g = 0c
assume f /. g = 0c ; :: thesis: contradiction
then f /. gg in {0c} by TARSKI:def 1;
hence contradiction by A2, A3, A4, A5, PARTFUN2:26; :: thesis: verum
end;
then lim ((f | X) /* s1) <> 0c by A6, A9, A10, A17;
hence ((f ^) | X) /* s1 is convergent by A11, A15, A20, COMSEQ_2:34; :: thesis: lim (((f ^) | X) /* s1) = ((f ^) | X) /. g
(f | X) /. g = lim ((f | X) /* s1) by A6, A9, A10;
hence lim (((f ^) | X) /* s1) = ((f | X) /. g) " by A11, A17, A21, A15, A20, COMSEQ_2:35
.= (f /. g) " by A16, PARTFUN2:15
.= (f ^) /. gg by A4, A5, CFUNCT_1:def 2
.= ((f ^) | X) /. g by A7, PARTFUN2:15 ;
:: thesis: verum
end;
hence (f ^) | X is_continuous_in g by A7; :: thesis: verum