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