for m being non zero Element of NAT
for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL-NS m),REAL st f = g & Z c= dom f holds
( f is_continuous_on Z iff for s being sequence of (REAL-NS m) st rng s c= Z & s is convergent & lim s in Z holds
( g /* s is convergent & g /. (lim s) = lim (g /* s) ) )