i ^2 in NAT by INT_1:3, XREAL_1:63;
hence i ^2 is natural ; :: thesis: verum