let m be non zero Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL-NS m),REAL st f = g holds
( ( Z c= dom f & f is_continuous_on Z ) iff g is_continuous_on Z )
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL-NS m),REAL st f = g holds
( ( Z c= dom f & f is_continuous_on Z ) iff g is_continuous_on Z )
let f be PartFunc of (REAL m),REAL; :: thesis: for g being PartFunc of (REAL-NS m),REAL st f = g holds
( ( Z c= dom f & f is_continuous_on Z ) iff g is_continuous_on Z )
let g be PartFunc of (REAL-NS m),REAL; :: thesis: ( f = g implies ( ( Z c= dom f & f is_continuous_on Z ) iff g is_continuous_on Z ) )
assume A1: f = g ; :: thesis: ( ( Z c= dom f & f is_continuous_on Z ) iff g is_continuous_on Z )

hereby :: thesis: ( g is_continuous_on Z implies ( Z c= dom f & f is_continuous_on Z ) )

assume A2: Z c= dom f ; :: thesis: ( f is_continuous_on Z implies g is_continuous_on Z )
assume A3: f is_continuous_on Z ; :: thesis: g is_continuous_on Z

now :: thesis: for y0 being Point of (REAL-NS m)
for r being Real st y0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )

let y0 be Point of (REAL-NS m); :: thesis: for r being Real st y0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )
let r be Real; :: thesis: ( y0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) )
reconsider x0 = y0 as Element of REAL m by REAL_NS1:def 4;
assume ( y0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )
then consider s being Real such that
A4: ( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by A2, A3, Th45;
take s = s; :: thesis: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )
thus 0 < s by A4; :: thesis: for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r
let y1 be Point of (REAL-NS m); :: thesis: ( y1 in Z & ||.(y1 - y0).|| < s implies |.((g /. y1) - (g /. y0)).| < r )
assume A5: ( y1 in Z & ||.(y1 - y0).|| < s ) ; :: thesis: |.((g /. y1) - (g /. y0)).| < r
reconsider x1 = y1 as Element of REAL m by REAL_NS1:def 4;
||.(y1 - y0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
hence |.((g /. y1) - (g /. y0)).| < r by A1, A5, A4; :: thesis: verum

end;

hence g is_continuous_on Z by A1, A2, NFCONT_1:20; :: thesis: verum

end;

assume A6: g is_continuous_on Z ; :: thesis: ( Z c= dom f & f is_continuous_on Z )
then A7: Z c= dom f by A1, NFCONT_1:20;

now :: thesis: for x0 being Element of REAL m
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )

let x0 be Element of REAL m; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
assume ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
then consider s being Real such that
A8: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in Z & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) by A6, NFCONT_1:20;
take s = s; :: thesis: ( 0 < s & ( for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) )
thus 0 < s by A8; :: thesis: for x1 being Element of REAL m st x1 in Z & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r
let x1 be Element of REAL m; :: thesis: ( x1 in Z & |.(x1 - x0).| < s implies |.((f /. x1) - (f /. x0)).| < r )
assume A9: ( x1 in Z & |.(x1 - x0).| < s ) ; :: thesis: |.((f /. x1) - (f /. x0)).| < r
reconsider y1 = x1 as Point of (REAL-NS m) by REAL_NS1:def 4;
||.(y1 - y0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5;
hence |.((f /. x1) - (f /. x0)).| < r by A1, A9, A8; :: thesis: verum

end;

hence ( Z c= dom f & f is_continuous_on Z ) by A7, Th45; :: thesis: verum