:: deftheorem Def18 defines plus FOMODEL0:def 18 :
for b₁ being Function of COMPLEX,COMPLEX holds
( b₁ = plus iff for z being Complex holds b₁ . z = z + 1 );