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 )

( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; :: thesis: f | X is continuous

( 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 A10:
for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
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) )

( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; :: thesis: verum

end;( 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) )

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) )

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;

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

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

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

( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) ; :: thesis: verum

( 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

hence
f | X is continuous
; :: thesis: verumf | 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

end;.= 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) )

hence
f | X is_continuous_in x1
; :: thesis: verum( (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) )

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

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

(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