let i1, i2 be Nat; :: thesis: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) implies i1 = i2 )
assume A2: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) ) ; :: thesis: i1 = i2
A3: 2 |^ n <> 0 by NEWTON:83;
then i1 = (i1 / (2 |^ n)) * (2 |^ n) by XCMPLX_1:87
.= i2 by A2, A3, XCMPLX_1:87 ;
hence i1 = i2 ; :: thesis: verum