let m be non zero Element of NAT ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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) ) )

hereby :: thesis: ( ( 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) ) ) implies f is_continuous_on Z )

assume f is_continuous_on Z ; :: thesis: for s1 being sequence of (REAL-NS m) st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( g /* s1 is convergent & g /. (lim s1) = lim (g /* s1) )
then g is_continuous_on Z by A2, Th42, A1;
hence for s1 being sequence of (REAL-NS m) st rng s1 c= Z & s1 is convergent & lim s1 in Z holds
( g /* s1 is convergent & g /. (lim s1) = lim (g /* s1) ) by Th2; :: thesis: verum

end;

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) ) ; :: thesis: f is_continuous_on Z
then g is_continuous_on Z by A1, A2, Th2;
hence f is_continuous_on Z by Th42, A1; :: thesis: verum