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