:: deftheorem defines diffcomplex SEQ_4:def 3 :
diffcomplex = addcomplex * ((id COMPLEX),compcomplex);