for E, F, G being RealNormSpace
for f being PartFunc of [:E,F:],G
for Z being Subset of [:E,F:]
for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds
( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )