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

assume f is_continuous_in x0 ; :: thesis:
then consider g being PartFunc of REAL,(REAL-NS n) such that
A1: ( f = g & g is_continuous_in x0 ) ;
thus x0 in dom f by A1; :: thesis:
thus for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A2: ( 0 < s & ( for x1 being Real st x1 in dom g & |.(x1 - x0).| < s holds
||.((g /. x1) - (g /. x0)).|| < r ) ) by A1, NFCONT_3:8;
take s ; :: thesis:
thus 0 < s by A2; :: thesis:
let x1 be Real; :: thesis:
assume ( x1 in dom f & |.(x1 - x0).| < s ) ; :: thesis:
then A3: ||.((g /. x1) - (g /. x0)).|| < r by A1, A2;
( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by A1, REAL_NS1:def 4;
hence |.((f /. x1) - (f /. x0)).| < r by A3, REAL_NS1:1, REAL_NS1:5; :: thesis:

end;

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

let r be Real; :: thesis:
reconsider rr = r as Real ;
assume 0 < r ; :: thesis:
then consider s being Real such that
A5: 0 < s and
A6: for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < rr by A4;
take s = s; :: thesis:
thus 0 < s by A5; :: thesis:
let x1 be Real; :: thesis:
assume ( x1 in dom g & |.(x1 - x0).| < s ) ; :: thesis:
then A7: |.((f /. x1) - (f /. x0)).| < r by A6;
( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by REAL_NS1:def 4;
hence ||.((g /. x1) - (g /. x0)).|| < r by A7, REAL_NS1:1, REAL_NS1:5; :: thesis:

end;