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 A4: f | Z is_continuous_in lim s1 by A1, NFCONT_1:def 8;
dom (f | Z) = (dom f) /\ Z by PARTFUN2:15;
then A5: 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 A6: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | Z) /* s1) . n = (f | Z) /. (s1 . n) by A3, A5, FUNCT_2:109
.= f /. (s1 . n) by A3, A5, A6, PARTFUN2:15
.= (f /* s1) . n by A2, A3, FUNCT_2:109, XBOOLE_1:1 ; :: thesis: verum

end;

then A7: (f | Z) /* s1 = f /* s1 ;
f /. (lim s1) = (f | Z) /. (lim s1) by A3, A5, PARTFUN2:15;
hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A5, A4, A7, 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
A8: Z c= dom f and
A9: 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 A10: dom (f | Z) = Z by A8, 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 A11: 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 A12: ( 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 A13: s1 . n in rng s1 by FUNCT_1:3;
thus ((f | Z) /* s1) . n = (f | Z) /. (s1 . n) by A12, FUNCT_2:109
.= f /. (s1 . n) by A12, A13, PARTFUN2:15
.= (f /* s1) . n by A8, A10, A12, FUNCT_2:109, XBOOLE_1:1 ; :: thesis: verum

end;

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

end;

hence f | Z is_continuous_in x1 by A11, A10, NFCONT_1:def 6; :: thesis: verum

end;

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