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