dom (F | A) is finite by Th13, RELAT_1:87;
hence F | A is finite by Th29; :: thesis: verum