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