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 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 A4: 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 A4, A3;
hence g | Z is_continuous_in x0 by A1, NFCONT_4:21; :: thesis: verum
end;
hence g is_continuous_on Z by A1, A2, NFCONT_1:def 8; :: thesis: verum
end;
assume A5: g is_continuous_on Z ; :: thesis: ( Z c= dom f & f is_continuous_on Z )
hence Z c= dom f by A1, 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 A6: 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 A6, A5, NFCONT_1:def 8;
hence f | Z is_continuous_in x0 by A1, NFCONT_4:21; :: thesis: verum