(
n
is
finite
&
n
,
seq
(
m
,
n
)
are_equipotent
)
by
Th6
;
hence
seq
(
m
,
n
) is
finite
by
CARD_1:38
;
:: thesis:
verum