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