:: deftheorem defines partdiff NDIFF_5:def 7 :
for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for x being Point of (product G) holds partdiff (f,x,i) = diff ((f * (reproj ((In (i,(dom G))),x))),((proj (In (i,(dom G)))) . x));