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