let m, n be non empty Element of NAT ; :: thesis: for F being PartFunc of ,
for G being PartFunc of ,
for x being Point of
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let F be PartFunc of ,; :: thesis: for G being PartFunc of ,
for x being Point of
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let G be PartFunc of ,; :: thesis: for x being Point of
for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let x be Point of ; :: thesis: for y being Element of REAL m st F = G & x = y holds
( F is_differentiable_in x iff G is_differentiable_in y )
let y be Element of REAL m; :: thesis: ( F = G & x = y implies ( F is_differentiable_in x iff G is_differentiable_in y ) )
assume that
A1: F = G and
A2: x = y ; :: thesis: ( F is_differentiable_in x iff G is_differentiable_in y )

now

assume G is_differentiable_in y ; :: thesis: F is_differentiable_in x
then ex f1 being PartFunc of , ex y1 being Point of st
( G = f1 & y = y1 & f1 is_differentiable_in y1 ) by Def7;
hence F is_differentiable_in x by A1, A2; :: thesis: verum

end;

hence ( F is_differentiable_in x iff G is_differentiable_in y ) by A1, A2, Def7; :: thesis: verum