theorem :: EUCLID_7:41

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