:: deftheorem defines - SEQ_4:def 7 :
for z1, z2 being FinSequence of COMPLEX holds z1 - z2 = diffcomplex .: (z1,z2);