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