consider k being Nat such that
A: card the carrier of R = k ;
card the carrier of (R ^* n) = k |^ n by A, Fin1;
hence R ^* n is finite ; :: thesis: verum