let i be Element of NAT ; :: thesis:
let f be PartFunc of (REAL i),REAL; :: thesis:
let x0 be Element of REAL i; :: thesis:

assume f is_continuous_in x0 ; :: thesis:
then consider y0 being Point of (REAL-NS i), g being PartFunc of (REAL-NS i),REAL such that
A1: ( x0 = y0 & f = g & g is_continuous_in y0 ) by NFCONT_4:def 4;
thus x0 in dom f by A1, NFCONT_1:8; :: thesis:
let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A2: ( 0 < s & ( for y1 being Point of (REAL-NS i) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) by A1, NFCONT_1:8;
take s = s; :: thesis:
thus 0 < s by A2; :: thesis:
let a be Element of REAL i; :: thesis:
assume A3: ( a in dom f & |.(a - x0).| < s ) ; :: thesis:
reconsider y1 = a as Point of (REAL-NS i) by REAL_NS1:def 4;
||.(y1 - y0).|| = |.(a - x0).| by A1, REAL_NS1:1, REAL_NS1:5;
hence |.((f /. a) - (f /. x0)).| < r by A1, A2, A3; :: thesis:

end;

assume A4: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for a being Element of REAL i st a in dom f & |.(a - x0).| < s holds
|.((f /. a) - (f /. x0)).| < r ) ) ) ) ; :: thesis:
reconsider y0 = x0 as Point of (REAL-NS i) by REAL_NS1:def 4;
reconsider g = f as PartFunc of (REAL-NS i),REAL by REAL_NS1:def 4;

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A5: ( 0 < s & ( for a being Element of REAL i st a in dom f & |.(a - x0).| < s holds
|.((f /. a) - (f /. x0)).| < r ) ) by A4;
take s = s; :: thesis:
thus 0 < s by A5; :: thesis:

let y1 be Point of (REAL-NS i); :: thesis:
assume A6: ( y1 in dom g & ||.(y1 - y0).|| < s ) ; :: thesis:
reconsider a = y1 as Element of REAL i by REAL_NS1:def 4;
||.(y1 - y0).|| = |.(a - x0).| by REAL_NS1:1, REAL_NS1:5;
hence |.((g /. y1) - (g /. y0)).| < r by A5, A6; :: thesis:

end;