:: deftheorem Def5 defines diff NDIFF_6:def 5 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for b₅ being Function holds
( b₅ = diff (f,Z) iff ( dom b₅ = NAT & b₅ . 0 = f | Z & ( for i being Nat holds b₅ . (i + 1) = (modetrans ((b₅ . i),S,(diff_SP (i,S,T)))) `| Z ) ) );