let i1, i2 be Element of NAT ; :: thesis: ( x = i1 / (2 |^ n) & x = i2 / (2 |^ n) implies i1 = i2 )
assume that
A2: x = i1 / (2 |^ n) and
A3: x = i2 / (2 |^ n) ; :: thesis: i1 = i2
A4: 2 |^ n <> 0 by NEWTON:102;
then i1 = (i1 / (2 |^ n)) * (2 |^ n) by XCMPLX_1:88
.= i2 by A2, A3, A4, XCMPLX_1:88 ;
hence i1 = i2 ; :: thesis: verum