let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st f | X is continuous & f " {0 } = {} holds
(f ^ ) | X is continuous
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | X is continuous & f " {0 } = {} implies (f ^ ) | X is continuous )
assume that
A1: f | X is continuous and
A2: f " {0 } = {} ; :: thesis: (f ^ ) | X is continuous
A3: dom (f ^ ) = (dom f) \ {} by A2, RFUNCT_1:def 8
.= dom f ;
let r be real number ; :: according to FCONT_1:def 2 :: thesis: ( r in dom ((f ^ ) | X) implies (f ^ ) | X is_continuous_in r )
assume A4: r in dom ((f ^ ) | X) ; :: thesis: (f ^ ) | X is_continuous_in r
then A5: r in dom (f ^ ) by RELAT_1:86;
r in X by A4, RELAT_1:86;
then A6: r in dom (f | X) by A3, A5, RELAT_1:86;
then A7: f | X is_continuous_in r by A1, Def2;

now

A8: now

assume f . r = 0 ; :: thesis: contradiction
then f . r in {0 } by TARSKI:def 1;
hence contradiction by A2, A3, A5, FUNCT_1:def 13; :: thesis: verum

end;

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom ((f ^ ) | X) & s1 is convergent & lim s1 = r implies ( ((f ^ ) | X) /* s1 is convergent & lim (((f ^ ) | X) /* s1) = ((f ^ ) | X) . r ) )
assume that
A9: rng s1 c= dom ((f ^ ) | X) and
A10: ( s1 is convergent & lim s1 = r ) ; :: thesis: ( ((f ^ ) | X) /* s1 is convergent & lim (((f ^ ) | X) /* s1) = ((f ^ ) | X) . r )
rng s1 c= (dom (f ^ )) /\ X by A9, RELAT_1:90;
then A11: rng s1 c= dom (f | X) by A3, RELAT_1:90;
then A12: (f | X) /* s1 is convergent by A7, A10, Def1;

now

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

A15: now

assume f . (s1 . n) = 0 ; :: thesis: contradiction
then f . (s1 . n) in {0 } by TARSKI:def 1;
hence contradiction by A2, A14, A13, FUNCT_1:def 13; :: thesis: verum

end;

((f | X) /* s1) . n = (f | X) . (s1 . n) by A11, FUNCT_2:185
.= f . (s1 . n) by A11, A13, FUNCT_1:70 ;
hence ((f | X) /* s1) . n <> 0 by A15; :: thesis: verum

end;

then A16: (f | X) /* s1 is non-empty by SEQ_1:7;

now

let n be Element of NAT ; :: thesis: (((f ^ ) | X) /* s1) . n = (((f | X) /* s1) " ) . n
A17: s1 . n in rng s1 by VALUED_0:28;
then s1 . n in dom ((f ^ ) | X) by A9;
then s1 . n in (dom (f ^ )) /\ X by RELAT_1:90;
then A18: s1 . n in dom (f ^ ) by XBOOLE_0:def 4;
thus (((f ^ ) | X) /* s1) . n = ((f ^ ) | X) . (s1 . n) by A9, FUNCT_2:185
.= (f ^ ) . (s1 . n) by A9, A17, FUNCT_1:70
.= (f . (s1 . n)) " by A18, RFUNCT_1:def 8
.= ((f | X) . (s1 . n)) " by A11, A17, FUNCT_1:70
.= (((f | X) /* s1) . n) " by A11, FUNCT_2:185
.= (((f | X) /* s1) " ) . n by VALUED_1:10 ; :: thesis: verum

end;

then A19: ((f ^ ) | X) /* s1 = ((f | X) /* s1) " by FUNCT_2:113;
A20: (f | X) . r = f . r by A6, FUNCT_1:70;
then lim ((f | X) /* s1) <> 0 by A7, A10, A11, A8, Def1;
hence ((f ^ ) | X) /* s1 is convergent by A12, A16, A19, SEQ_2:35; :: thesis: lim (((f ^ ) | X) /* s1) = ((f ^ ) | X) . r
(f | X) . r = lim ((f | X) /* s1) by A7, A10, A11, Def1;
hence lim (((f ^ ) | X) /* s1) = ((f | X) . r) " by A12, A20, A8, A16, A19, SEQ_2:36
.= (f . r) " by A6, FUNCT_1:70
.= (f ^ ) . r by A5, RFUNCT_1:def 8
.= ((f ^ ) | X) . r by A4, FUNCT_1:70 ;
:: thesis: verum

end;

hence (f ^ ) | X is_continuous_in r by Def1; :: thesis: verum