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 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 A2: <>* (f | Z) = g | Z by Th5;
hence ( Z c= dom f & f is_continuous_on Z implies g is_continuous_on Z ) by A1, Th3, Th37; :: thesis: ( g is_continuous_on Z implies ( Z c= dom f & f is_continuous_on Z ) )
assume A3: g is_continuous_on Z ; :: thesis: ( Z c= dom f & f is_continuous_on Z )
hence Z c= dom f by Th3, 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
hence f | Z is_continuous_in x0 by A3, A2, Th37; :: thesis: verum