let i be Integer; :: thesis: i is dyadic-like
2 |^ 0 = 1 by NEWTON:4;
then i = i / (2 |^ 0) ;
hence i is dyadic-like ; :: thesis: verum