:: deftheorem defines COMPLEX NUMBERS:def 2 :
COMPLEX = ((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL;