reconsider p = p as Tuple of i, ;
reconsider q = q as Tuple of j, ;
p ^ q is Tuple of i + j, by FINSEQ_2:127;
hence p ^ q is Tuple of (i + j),RAS by FINSEQ_2:151; :: thesis: verum