( 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