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 A1: 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 A2: 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 :: 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) )

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 that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X ; :: thesis: ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) )
A6: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then A7: f | X is_continuous_in lim s1 by A2, A5;

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

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

end;

then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
f . (lim s1) = (f | X) . (lim s1) by A5, A6, FUNCT_1:47
.= lim (f /* s1) by A3, A4, A6, A7, A9 ;
hence ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) by A3, A4, A6, A7, A9; :: 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 A10: 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 :: thesis: for x1 being Real st x1 in dom (f | X) holds
f | X is_continuous_in x1

A11: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
let x1 be Real; :: thesis: ( x1 in dom (f | X) implies f | X is_continuous_in x1 )
assume A12: x1 in dom (f | X) ; :: thesis: f | X is_continuous_in x1

now :: thesis: for s1 being Real_Sequence st rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 holds
( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) )

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 that
A13: rng s1 c= dom (f | X) and
A14: s1 is convergent and
A15: lim s1 = x1 ; :: thesis: ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) )

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

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

end;

then A17: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
(f | X) . (lim s1) = f . (lim s1) by A12, A15, FUNCT_1:47
.= lim ((f | X) /* s1) by A10, A12, A11, A13, A14, A15, A17 ;
hence ( (f | X) /* s1 is convergent & (f | X) . x1 = lim ((f | X) /* s1) ) by A10, A12, A11, A13, A14, A15, A17; :: thesis: verum

end;

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

end;

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