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