:: deftheorem Def1 defines R2-to-C INTEGR1C:def 1 :
for b₁ being Function of [:REAL,REAL:],COMPLEX holds
( b₁ = R2-to-C iff for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b₁ . [a,b] = a + (b * <i>) );