sqrt (1 ^2) = 1 by Def2;
hence sqrt 1 = 1 ; :: thesis: verum