:: deftheorem Def4 defines linear CFDIFF_1:def 4 :
for IT being PartFunc of COMPLEX,COMPLEX holds
( IT is linear iff ex a being Complex st
for z being Complex holds IT /. z = a * z );