let n be Nat; :: thesis: ( Mersenne n = 1 implies n = 1 )
assume A1: Mersenne n = 1 ; :: thesis: n = 1
Mersenne n = (2 |^ n) - 1 by GR_CY_3:def 3;
then 2 to_power n = 2 to_power 1 by A1;
hence n = 1 by POWER:50; :: thesis: verum