card (r * A) c= card A by Lm4;
hence r * A is finite ; :: thesis: verum