let n be Element of NAT ; :: thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let x0 be real number ; :: thesis: for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

hereby :: thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_in x0 )

assume f is_continuous_in x0 ; :: thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) )
then consider g being PartFunc of REAL, the carrier of (REAL-NS n) such that
A2: ( f = g & g is_continuous_in x0 ) by Def1;
thus x0 in dom f by A2, NFCONT_3:8; :: thesis: for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) :: thesis: verum

proof

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

end;

end;

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

now

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

end;

then g is_continuous_in x0 by A1, NFCONT_3:8;
hence f is_continuous_in x0 by Def1; :: thesis: verum