let Z be set ; :: thesis:
let S be RealNormSpace; :: thesis:
let f be PartFunc of S,REAL; :: thesis:
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:

assume A1: f is_continuous_on Z ; :: thesis:
then A2: Z c= dom f by NFCONT_1:def 8;

let s1 be sequence of S; :: thesis:
assume A3: ( rng s1 c= Z & s1 is convergent & lim s1 in Z ) ; :: thesis:
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;

let n be Element of NAT ; :: thesis:
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:

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:

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:

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:
dom (f | Z) = (dom f) /\ Z by PARTFUN2:15;
then A10: dom (f | Z) = Z by A8, XBOOLE_1:28;

let x1 be Point of S; :: thesis:
assume A11: x1 in Z ; :: thesis:

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

let n be Element of NAT ; :: thesis:
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:

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:

end;

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

end;

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