theorem Th12: :: NDIFF_6:12

for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for i being Nat holds (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T))