let i be Element of NAT ; :: thesis:
let f be PartFunc of (REAL i),REAL; :: thesis:
let g be PartFunc of (REAL-NS i),REAL; :: thesis:
let x be Element of REAL i; :: thesis:
let y be Point of (REAL-NS i); :: thesis:
assume A1: ( f = g & x = y ) ; :: thesis:

hereby :: thesis:

assume f is_continuous_in x ; :: thesis:
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:

end;

hereby :: thesis:

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:
then g is_continuous_in y by NFCONT_1:def 6;
hence f is_continuous_in x by A1, NFCONT_4:21; :: thesis:

end;