reconsider b = |.a.| as Nat ;
( b = a or b = - a ) by COMPLEX1:71;
then ( b * b = a * a or b * b = (- a) * (- a) ) ;
then a * a = b ^2 by SQUARE_1:def 1;
hence a * a is square ; :: thesis: verum