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