for a being Real holds sqrt (a ^2) = |.a.| by Lm28;