theorem Th8: :: NDIFF_6:8

for S, T being RealNormSpace
for i being Nat holds (diff_SP (S,T)) . i is RealNormSpace