let a be Real; :: thesis: |.a.| ^2 = a ^2
( |.a.| = a or |.a.| = - a ) by Th71;
hence |.a.| ^2 = a ^2 ; :: thesis: verum