let m be non empty Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) 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 m),(REAL 1) 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 m),(REAL 1) 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 m),(REAL 1); :: 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 )
then A0: <>* (f | Z) = g | Z by LMXTh1;

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

assume AK: Z c= dom f ; :: thesis: ( f is_continuous_on Z implies g is_continuous_on Z )
assume A2: f is_continuous_on Z ; :: thesis: g is_continuous_on Z
A3: Z c= dom g by LMXTh0, A1, AK;

now :: thesis: for x0 being Element of REAL m st x0 in Z holds
g | Z is_continuous_in x0

let x0 be Element of REAL m; :: thesis: ( x0 in Z implies g | Z is_continuous_in x0 )
assume x0 in Z ; :: thesis: g | Z is_continuous_in x0
then f | Z is_continuous_in x0 by A2, XDef7;
hence g | Z is_continuous_in x0 by A0, XTh35; :: thesis: verum

end;

hence g is_continuous_on Z by A3, PDIFF_7:def 7; :: thesis: verum

end;

assume A5: g is_continuous_on Z ; :: thesis: ( Z c= dom f & f is_continuous_on Z )
then Z c= dom g by PDIFF_7:def 7;
hence Z c= dom f by LMXTh0, A1; :: thesis: f is_continuous_on Z
let x0 be Element of REAL m; :: according to PDIFF_9:def 2 :: thesis: ( x0 in Z implies f | Z is_continuous_in x0 )
assume x0 in Z ; :: thesis: f | Z is_continuous_in x0
then g | Z is_continuous_in x0 by A5, PDIFF_7:def 7;
hence f | Z is_continuous_in x0 by A0, XTh35; :: thesis: verum