R1 - R2 = diffcomplex .: R1,R2 by SEQ_4:def 10;
hence R1 - R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:140; :: thesis: verum