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

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

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

then sqrt (a ^2) = a by SQUARE_1:22;
hence sqrt (a ^2) = |.a.| by A1, Th43; :: thesis: verum

end;

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

then |.a.| = - a by Lm27;
hence sqrt (a ^2) = |.a.| by A2, SQUARE_1:23; :: thesis: verum

end;

end;