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 2

.= dom f ;

let r be Real; :: 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:57;

r in X by A4;

then A6: r in dom (f | X) by A3, A5, RELAT_1:57;

then A7: f | X is_continuous_in r by A1;

(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 2

.= dom f ;

let r be Real; :: 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:57;

r in X by A4;

then A6: r in dom (f | X) by A3, A5, RELAT_1:57;

then A7: f | X is_continuous_in r by A1;

now :: thesis: for s1 being Real_Sequence st rng s1 c= dom ((f ^) | X) & s1 is convergent & lim s1 = r holds

( ((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:61;

then A11: rng s1 c= dom (f | X) by A3, RELAT_1:61;

then A12: (f | X) /* s1 is convergent by A7, A10;

A20: (f | X) . r = f . r by A6, FUNCT_1:47;

then lim ((f | X) /* s1) <> 0 by A7, A10, A11, A8;

hence ((f ^) | X) /* s1 is convergent by A12, A16, A19, SEQ_2:21; :: thesis: lim (((f ^) | X) /* s1) = ((f ^) | X) . r

(f | X) . r = lim ((f | X) /* s1) by A7, A10, A11;

hence lim (((f ^) | X) /* s1) = ((f | X) . r) " by A12, A20, A8, A16, A19, SEQ_2:22

.= (f . r) " by A6, FUNCT_1:47

.= (f ^) . r by A5, RFUNCT_1:def 2

.= ((f ^) | X) . r by A4, FUNCT_1:47 ;

:: thesis: verum

end;

hence
(f ^) | X is_continuous_in r
; :: thesis: verum( ((f ^) | X) /* s1 is convergent & lim (((f ^) | X) /* s1) = ((f ^) | X) . r )

A8: now :: thesis: not f . r = 0

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
f . r = 0
; :: thesis: contradiction

then f . r in {0} by TARSKI:def 1;

hence contradiction by A2, A3, A5, FUNCT_1:def 7; :: thesis: verum

end;then f . r in {0} by TARSKI:def 1;

hence contradiction by A2, A3, A5, FUNCT_1:def 7; :: thesis: verum

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:61;

then A11: rng s1 c= dom (f | X) by A3, RELAT_1:61;

then A12: (f | X) /* s1 is convergent by A7, A10;

now :: thesis: for n being Nat holds ((f | X) /* s1) . n <> 0

then A16:
(f | X) /* s1 is non-zero
by SEQ_1:5;let n be 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:61, XBOOLE_1:17;

then A14: rng s1 c= dom f ;

then ((f | X) /* s1) . n = (f | X) . (s1 . n) by A11, FUNCT_2:108

.= f . (s1 . n) by A11, A13, FUNCT_1:47 ;

hence ((f | X) /* s1) . n <> 0 by A15; :: thesis: verum

end;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:61, XBOOLE_1:17;

then A14: rng s1 c= dom f ;

A15: now :: thesis: not f . (s1 . n) = 0

n in NAT
by ORDINAL1:def 12;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 7; :: thesis: verum

end;then f . (s1 . n) in {0} by TARSKI:def 1;

hence contradiction by A2, A14, A13, FUNCT_1:def 7; :: thesis: verum

then ((f | X) /* s1) . n = (f | X) . (s1 . n) by A11, FUNCT_2:108

.= f . (s1 . n) by A11, A13, FUNCT_1:47 ;

hence ((f | X) /* s1) . n <> 0 by A15; :: thesis: verum

now :: thesis: for n being Element of NAT holds (((f ^) | X) /* s1) . n = (((f | X) /* s1) ") . n

then A19:
((f ^) | X) /* s1 = ((f | X) /* s1) "
by FUNCT_2:63;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:61;

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:108

.= (f ^) . (s1 . n) by A9, A17, FUNCT_1:47

.= (f . (s1 . n)) " by A18, RFUNCT_1:def 2

.= ((f | X) . (s1 . n)) " by A11, A17, FUNCT_1:47

.= (((f | X) /* s1) . n) " by A11, FUNCT_2:108

.= (((f | X) /* s1) ") . n by VALUED_1:10 ; :: thesis: verum

end;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:61;

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:108

.= (f ^) . (s1 . n) by A9, A17, FUNCT_1:47

.= (f . (s1 . n)) " by A18, RFUNCT_1:def 2

.= ((f | X) . (s1 . n)) " by A11, A17, FUNCT_1:47

.= (((f | X) /* s1) . n) " by A11, FUNCT_2:108

.= (((f | X) /* s1) ") . n by VALUED_1:10 ; :: thesis: verum

A20: (f | X) . r = f . r by A6, FUNCT_1:47;

then lim ((f | X) /* s1) <> 0 by A7, A10, A11, A8;

hence ((f ^) | X) /* s1 is convergent by A12, A16, A19, SEQ_2:21; :: thesis: lim (((f ^) | X) /* s1) = ((f ^) | X) . r

(f | X) . r = lim ((f | X) /* s1) by A7, A10, A11;

hence lim (((f ^) | X) /* s1) = ((f | X) . r) " by A12, A20, A8, A16, A19, SEQ_2:22

.= (f . r) " by A6, FUNCT_1:47

.= (f ^) . r by A5, RFUNCT_1:def 2

.= ((f ^) | X) . r by A4, FUNCT_1:47 ;

:: thesis: verum