let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f holds
( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f implies ( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) )
assume Z: X c= dom f ; :: thesis: ( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
thus ( f | X is continuous implies for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) :: thesis: ( ( for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ) implies f | X is continuous )

proof

assume A1: f | X is continuous ; :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) )

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
assume A3: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) )
A4: dom (f | X) = (dom f) /\ X by RELAT_1:90
.= X by Z, XBOOLE_1:28 ;
then A5: f | X is_continuous_in lim s1 by A1, A3, Def2;

now

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n = (f /* s1) . n
A6: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) . (s1 . n) by A3, A4, FUNCT_2:185
.= f . (s1 . n) by A3, A4, A6, FUNCT_1:70
.= (f /* s1) . n by A3, Z, FUNCT_2:185, XBOOLE_1:1 ; :: thesis: verum

end;

then A8: (f | X) /* s1 = f /* s1 by FUNCT_2:113;
f . (lim s1) = (f | X) . (lim s1) by A3, A4, FUNCT_1:70
.= lim (f /* s1) by A3, A4, A5, A8, Def1 ;
hence ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) by A3, A4, A5, A8, Def1; :: thesis: verum

end;

hence for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; :: thesis: verum

end;

assume A9: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; :: thesis: f | X is continuous

now

let x1 be real number ; :: thesis: ( x1 in dom (f | X) implies f | X is_continuous_in x1 )
assume A10: x1 in dom (f | X) ; :: thesis: f | X is_continuous_in x1
A11: dom (f | X) = (dom f) /\ X by RELAT_1:90
.= X by Z, XBOOLE_1:28 ;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 implies ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) ) )
assume A12: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 ) ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) )

now

let n be Element of NAT ; :: thesis: ((f | X) /* s1) . n = (f /* s1) . n
A13: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) . (s1 . n) by A12, FUNCT_2:185
.= f . (s1 . n) by A12, A13, FUNCT_1:70
.= (f /* s1) . n by A11, A12, Z, FUNCT_2:185, XBOOLE_1:1 ; :: thesis: verum

end;

then A15: (f | X) /* s1 = f /* s1 by FUNCT_2:113;
(f | X) . (lim s1) = f . (lim s1) by A10, A12, FUNCT_1:70
.= lim ((f | X) /* s1) by A9, A10, A11, A12, A15 ;
hence ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) ) by A9, A10, A11, A12, A15; :: thesis: verum

end;

hence f | X is_continuous_in x1 by Def1; :: thesis: verum

end;

hence f | X is continuous by Def2; :: thesis: verum