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