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_differentiable_on Z ) iff g is_differentiable_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_differentiable_on Z ) iff g is_differentiable_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_differentiable_on Z ) iff g is_differentiable_on Z )
let g be PartFunc of (REAL m),(REAL 1); :: thesis: ( <>* f = g implies ( ( Z c= dom f & f is_differentiable_on Z ) iff g is_differentiable_on Z ) )
assume A1: <>* f = g ; :: thesis: ( ( Z c= dom f & f is_differentiable_on Z ) iff g is_differentiable_on Z )
A2: dom (<>* f) = dom f by Th3;
hereby :: thesis: ( g is_differentiable_on Z implies ( Z c= dom f & f is_differentiable_on Z ) )
assume A3: Z c= dom f ; :: thesis: ( f is_differentiable_on Z implies g is_differentiable_on Z )
assume A4: f is_differentiable_on Z ; :: thesis: g is_differentiable_on Z
A5: Z c= dom g by A3, Th3, A1;
now :: thesis: for x being Element of REAL m st x in Z holds
g | Z is_differentiable_in x
let x be Element of REAL m; :: thesis: ( x in Z implies g | Z is_differentiable_in x )
assume x in Z ; :: thesis: g | Z is_differentiable_in x
then f | Z is_differentiable_in x by A4;
hence g | Z is_differentiable_in x by A1, Th5; :: thesis: verum
end;
hence g is_differentiable_on Z by A5, PDIFF_6:def 4; :: thesis: verum
end;
assume A6: g is_differentiable_on Z ; :: thesis: ( Z c= dom f & f is_differentiable_on Z )
hence Z c= dom f by A2, A1, PDIFF_6:def 4; :: thesis: f is_differentiable_on Z
hereby :: according to PDIFF_9:def 3 :: thesis: verum
let x be Element of REAL m; :: thesis: ( x in Z implies f | Z is_differentiable_in x )
assume x in Z ; :: thesis: f | Z is_differentiable_in x
then g | Z is_differentiable_in x by A6, PDIFF_6:def 4;
hence f | Z is_differentiable_in x by A1, Th5; :: thesis: verum
end;