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-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 AS: 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 P2: Z c= dom f ; :: thesis: ( f is_continuous_on Z implies g is_continuous_on Z )
assume P0: f is_continuous_on Z ; :: thesis: g is_continuous_on Z

now :: thesis: for x0 being Point of (REAL-NS m) st x0 in Z holds
g | Z is_continuous_in x0

let x0 be Point of (REAL-NS m); :: thesis: ( x0 in Z implies g | Z is_continuous_in x0 )
assume P3: x0 in Z ; :: thesis: g | Z is_continuous_in x0
reconsider y0 = x0 as Element of REAL m by REAL_NS1:def 4;
f | Z is_continuous_in y0 by P3, P0, XDef7;
hence g | Z is_continuous_in x0 by AS, NFCONT_4:21; :: thesis: verum

end;

hence g is_continuous_on Z by AS, P2, NFCONT_1:def 8; :: thesis: verum

end;

assume P1: g is_continuous_on Z ; :: thesis: ( Z c= dom f & f is_continuous_on Z )
hence Z c= dom f by AS, NFCONT_1:def 8; :: 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 P3: x0 in Z ; :: thesis: f | Z is_continuous_in x0
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
g | Z is_continuous_in y0 by P3, P1, NFCONT_1:def 8;
hence f | Z is_continuous_in x0 by AS, NFCONT_4:21; :: thesis: verum