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 ;
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
.= f . (s1 . n) by
.= (f /* s1) . n by ; :: thesis: verum
end;
then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
f . (lim s1) = (f | X) . (lim s1) by
.= 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 ;
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:
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
.= f . (s1 . n) by
.= (f /* s1) . n by ; :: thesis: verum
end;
then A17: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
(f | X) . (lim s1) = f . (lim s1) by
.= 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