theorem FinCar: :: MOEBIUS2:38

for p being Prime holds card (FreeGen p) c= card (BoolePrime p)