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