let n be non empty Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n)
for x being real number st h = f holds
( f is_differentiable_in x iff h is_differentiable_in x )
let f be PartFunc of REAL,(REAL n); :: thesis: for h being PartFunc of REAL,(REAL-NS n)
for x being real number st h = f holds
( f is_differentiable_in x iff h is_differentiable_in x )
let h be PartFunc of REAL,(REAL-NS n); :: thesis: for x being real number st h = f holds
( f is_differentiable_in x iff h is_differentiable_in x )
let x be real number ; :: thesis: ( h = f implies ( f is_differentiable_in x iff h is_differentiable_in x ) )
assume A1: h = f ; :: thesis: ( f is_differentiable_in x iff h is_differentiable_in x )

hereby :: thesis: ( h is_differentiable_in x implies f is_differentiable_in x )

assume f is_differentiable_in x ; :: thesis: h is_differentiable_in x
then ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_differentiable_in x ) by Def1;
hence h is_differentiable_in x by A1; :: thesis: verum

end;

thus ( h is_differentiable_in x implies f is_differentiable_in x ) by A1, Def1; :: thesis: verum