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