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