for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S holds
( (diff (f,Z)) . 0 = f | Z & (diff (f,Z)) . 1 = (f | Z) `| Z & (diff (f,Z)) . 2 = ((f | Z) `| Z) `| Z )