let n be mersenne Prime; :: thesis: ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 )
consider k being Nat such that
A1: n = Mersenne k by NUMPOLY1:def 12;
A3: k >= 1

proof

assume k < 1 ; :: thesis: contradiction
then k = 0 by NAT_1:14;
hence contradiction by A1, GR_CY_3:16; :: thesis: verum

end;

A2: Mersenne k = (2 |^ k) - 1 by GR_CY_3:def 3;
A4: n + 1 = 2 |^ k by A1, A2;
2 is Prime by INT_2:28;
then PrimeDivisors (2 |^ k) = {2} by A3, NUMBER12:50;
then T1: card (PrimeDivisors (n + 1)) = 1 by A4, CARD_2:42;
PrimeDivisors n = PrimeDivisors (n |^ 1)
.= {n} by NUMBER12:50 ;
hence ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) by T1, CARD_2:42; :: thesis: verum