:: deftheorem Def3 defines linear FDIFF_1:def 3 :
for IT being PartFunc of REAL,REAL holds
( IT is linear iff ( IT is total & ex r being Real st
for p being Real holds IT . p = r * p ) );