theorem Fin1: :: VECTSP13:31

for R being finite Ring
for n being Nat holds card the carrier of (R ^* n) = (card the carrier of R) |^ n