reconsider p = p as Tuple of i, the carrier of RAS ;
reconsider q = q as Tuple of j, the carrier of RAS ;
p ^ q is Tuple of i + j, the carrier of RAS by FINSEQ_2:107;
hence p ^ q is Tuple of (i + j),RAS by FINSEQ_2:131; :: thesis: verum