:: deftheorem Def2 defines linear NDIFF_3:def 2 :
for F being RealNormSpace
for IT being Function of REAL, the carrier of F holds
( IT is linear iff ex r being Point of F st
for p being Real holds IT /. p = p * r );