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