for n being Nat holds card (RN_Base n) = n by Lm5;