let Z be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of S,REAL holds
( f is_continuous_on Z iff ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
let S be RealNormSpace; :: thesis: for f being PartFunc of S,REAL holds
( f is_continuous_on Z iff ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
let f be PartFunc of S,REAL; :: thesis: ( f is_continuous_on Z iff ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) )
thus ( f is_continuous_on Z implies ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) :: thesis: ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) implies f is_continuous_on Z )

proof

assume A1: f is_continuous_on Z ; :: thesis: ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) )
then A2: Z c= dom f by NFCONT_1:def 8;

now :: thesis: for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )

let s1 be sequence of S; :: thesis: ( rng s1 c= Z & s1 is convergent & lim s1 in Z implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )
assume A3: ( rng s1 c= Z & s1 is convergent & lim s1 in Z ) ; :: thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )
then A6: f | Z is_continuous_in lim s1 by A1, NFCONT_1:def 8;
dom (f | Z) = (dom f) /\ Z by PARTFUN2:15;
then A7: dom (f | Z) = Z by A2, XBOOLE_1:28;

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

let n be Element of NAT ; :: thesis: ((f | Z) /* s1) . n = (f /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A8: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | Z) /* s1) . n = (f | Z) /. (s1 . n) by A3, A7, FUNCT_2:109
.= f /. (s1 . n) by A3, A7, A8, PARTFUN2:15
.= (f /* s1) . n by A2, A3, FUNCT_2:109, XBOOLE_1:1 ; :: thesis: verum

end;

then A9: (f | Z) /* s1 = f /* s1 by FUNCT_2:63;
f /. (lim s1) = (f | Z) /. (lim s1) by A3, A7, PARTFUN2:15;
hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A7, A6, A9, NFCONT_1:def 6; :: thesis: verum

end;

hence ( Z c= dom f & ( for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) by A1, NFCONT_1:def 8; :: thesis: verum

end;

assume that
A10: Z c= dom f and
A11: for s1 being sequence of S st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ; :: thesis: f is_continuous_on Z
dom (f | Z) = (dom f) /\ Z by PARTFUN2:15;
then A12: dom (f | Z) = Z by A10, XBOOLE_1:28;

now :: thesis: for x1 being Point of S st x1 in Z holds
f | Z is_continuous_in x1

let x1 be Point of S; :: thesis: ( x1 in Z implies f | Z is_continuous_in x1 )
assume A13: x1 in Z ; :: thesis: f | Z is_continuous_in x1

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

let s1 be sequence of S; :: thesis: ( rng s1 c= dom (f | Z) & s1 is convergent & lim s1 = x1 implies ( (f | Z) /* s1 is convergent & (f | Z) /. x1 = lim ((f | Z) /* s1) ) )
assume A14: ( rng s1 c= dom (f | Z) & s1 is convergent & lim s1 = x1 ) ; :: thesis: ( (f | Z) /* s1 is convergent & (f | Z) /. x1 = lim ((f | Z) /* s1) )

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

let n be Element of NAT ; :: thesis: ((f | Z) /* s1) . n = (f /* s1) . n
dom s1 = NAT by FUNCT_2:def 1;
then A17: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | Z) /* s1) . n = (f | Z) /. (s1 . n) by A14, FUNCT_2:109
.= f /. (s1 . n) by A14, A17, PARTFUN2:15
.= (f /* s1) . n by A10, A12, A14, FUNCT_2:109, XBOOLE_1:1 ; :: thesis: verum

end;

then A18: (f | Z) /* s1 = f /* s1 by FUNCT_2:63;
(f | Z) /. (lim s1) = f /. (lim s1) by A13, A12, A14, PARTFUN2:15;
hence ( (f | Z) /* s1 is convergent & (f | Z) /. x1 = lim ((f | Z) /* s1) ) by A11, A13, A12, A14, A18; :: thesis: verum

end;

hence f | Z is_continuous_in x1 by A13, A12, NFCONT_1:def 6; :: thesis: verum

end;

hence f is_continuous_on Z by A10, NFCONT_1:def 8; :: thesis: verum