let p be Prime; :: thesis: card (FreeGen p) c= 2 |^ p
A1: card (FreeGen p) c= card (BoolePrime p) by FinCar;
A2: card ((Seg p) /\ SetPrimes) <= card (Seg p) by NAT_1:43, XBOOLE_1:17;
card (BoolePrime p) = (card 2) |^ (card ((Seg p) /\ SetPrimes)) by CARD_FIN:4
.= 2 |^ (card ((Seg p) /\ SetPrimes)) ;
then card (BoolePrime p) <= 2 |^ (card (Seg p)) by PREPOWER:93, A2;
then card (BoolePrime p) <= 2 |^ p by FINSEQ_1:57;
then Segm (card (BoolePrime p)) c= Segm (2 |^ p) by NAT_1:39;
hence card (FreeGen p) c= 2 |^ p by A1; :: thesis: verum