for Z being set
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) ) ) ) )