consider k being Nat such that
A1: a = k ^2 by PYTHTRIP:def 3;
2 -root (k |^ 2) = k ;
hence 2 -root a is natural by A1, NEWTON:81; :: thesis: verum