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:127;
hence p ^ q is Tuple of (i + j),RAS by FINSEQ_2:151; :: thesis: verum