let a, z be Complex; :: thesis: ( z |^ 2 = a iff ( z = 2 -root a or z = - (2 -root a) ) )
A1: a = (2 -root a) |^ 2 by Th7
.= (2 -root a) * (2 -root a) by Th1 ;

hereby :: thesis: ( ( z = 2 -root a or z = - (2 -root a) ) implies z |^ 2 = a )

assume z |^ 2 = a ; :: thesis: ( not z = 2 -root a implies z = - (2 -root a) )
then A2: z * z = a by Th1;
assume not z = 2 -root a ; :: thesis: z = - (2 -root a)
then A3: z - (2 -root a) <> 0 ;
assume not z = - (2 -root a) ; :: thesis: contradiction
then z + (2 -root a) <> 0 ;
then (z - (2 -root a)) * (z + (2 -root a)) <> 0 by A3;
hence contradiction by A1, A2; :: thesis: verum

end;

assume ( z = 2 -root a or z = - (2 -root a) ) ; :: thesis: z |^ 2 = a
then (z * z) - ((2 -root a) * (2 -root a)) = 0 ;
hence z |^ 2 = a by A1, Th1; :: thesis: verum