let n1, n2, m2, m1 be Nat; :: thesis: ( (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) implies ( n1 = n2 & m1 = m2 ) )
A1: 2 |^ n1 <> 0 by Th3;
assume A2: (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) ; :: thesis: ( n1 = n2 & m1 = m2 )
then ( n1 <= n2 & n2 <= n1 ) by Lm1;
hence n1 = n2 by XXREAL_0:1; :: thesis: m1 = m2
then (2 * m1) + 1 = (2 * m2) + 1 by A2, A1, XCMPLX_1:5;
hence m1 = m2 ; :: thesis: verum