i * i = i ^2 by SQUARE_1:def 1;
hence i ^2 is integer ; :: thesis: verum