let a be real number ; :: thesis: sqrt (a ^2 ) = |.a.|

per cases ( 0 <= a or not 0 <= a ) ;

suppose 0 <= a ; :: thesis: sqrt (a ^2 ) = |.a.|

then ( sqrt (a ^2 ) = a & |.a.| = a ) by Th129, SQUARE_1:89;
hence sqrt (a ^2 ) = |.a.| ; :: thesis: verum

end;

suppose not 0 <= a ; :: thesis: sqrt (a ^2 ) = |.a.|

then ( |.a.| = - a & a < 0 ) by Lm23;
hence sqrt (a ^2 ) = |.a.| by SQUARE_1:90; :: thesis: verum

end;

end;