:: deftheorem defines COMPLEX SEQ_4:def 11 :
for n being Nat holds COMPLEX n = n -tuples_on COMPLEX;