let m be 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) ) )
let Z be 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) ) )
let f be 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) ) )
let g be PartFunc of (REAL-NS m),REAL; ( f = g & Z c= dom f implies ( 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) ) ) )
assume A1:
f = g
; ( not Z c= dom f or ( 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) ) ) )
assume A2:
Z c= dom f
; ( 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) ) )
assume
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) )
; f is_continuous_on Z
then
g is_continuous_on Z
by A1, A2, Th2;
hence
f is_continuous_on Z
by Th42, A1; verum