consider ix being Integer, nx being Nat such that
A2: x = ix / (2 |^ nx) by Th18;
consider iy being Integer, ny being Nat such that
A3: y = iy / (2 |^ ny) by Th18;
( x + y = ((ix * (2 |^ ny)) + (iy * (2 |^ nx))) / ((2 |^ nx) * (2 |^ ny)) & (2 |^ nx) * (2 |^ ny) = 2 |^ (nx + ny) ) by A2, A3, XCMPLX_1:116, NEWTON:8;
hence x + y is dyadic-like ; :: thesis: verum