theorem Th4: :: CARD_4:4

for n1, n2, m2, m1 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 & m1 = m2 )