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