let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL i),REAL
for g being PartFunc of (REAL-NS i),REAL
for x being Element of REAL i
for y being Point of (REAL-NS i) st f = g & x = y holds
( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )
let f be PartFunc of (REAL i),REAL; :: thesis: for g being PartFunc of (REAL-NS i),REAL
for x being Element of REAL i
for y being Point of (REAL-NS i) st f = g & x = y holds
( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )
let g be PartFunc of (REAL-NS i),REAL; :: thesis: for x being Element of REAL i
for y being Point of (REAL-NS i) st f = g & x = y holds
( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )
let x be Element of REAL i; :: thesis: for y being Point of (REAL-NS i) st f = g & x = y holds
( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )
let y be Point of (REAL-NS i); :: thesis: ( f = g & x = y implies ( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) ) )
assume A1: ( f = g & x = y ) ; :: thesis: ( f is_continuous_in x iff ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) )

hereby :: thesis: ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) implies f is_continuous_in x )

assume f is_continuous_in x ; :: thesis: ( y in dom g & ( for s1 being sequence of (REAL-NS i) st rng s1 c= dom g & s1 is convergent & lim s1 = y holds
( g /* s1 is convergent & g /. y = lim (g /* s1) ) ) )
then g is_continuous_in y by A1, NFCONT_4:21;
hence ( y in dom g & ( for s1 being sequence of (REAL-NS i) st rng s1 c= dom g & s1 is convergent & lim s1 = y holds
( g /* s1 is convergent & g /. y = lim (g /* s1) ) ) ) by NFCONT_1:def 6; :: thesis: verum

end;

hereby :: thesis: verum

assume ( y in dom g & ( for s being sequence of (REAL-NS i) st rng s c= dom g & s is convergent & lim s = y holds
( g /* s is convergent & g /. y = lim (g /* s) ) ) ) ; :: thesis: f is_continuous_in x
then g is_continuous_in y by NFCONT_1:def 6;
hence f is_continuous_in x by A1, NFCONT_4:21; :: thesis: verum

end;