let a, z be complex number ; :: thesis: ( z |^ 2 = a iff ( z = 2 -root a or z = - (2 -root a) ) )
A1: a = (2 -root a) |^ 2 by Th8
.= (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 A3: not z = 2 -root a ; :: thesis: z = - (2 -root a)
assume A4: not z = - (2 -root a) ; :: thesis: contradiction
( z - (2 -root a) <> 0 & z + (2 -root a) <> 0 ) by A3, A4;
then (z - (2 -root a)) * (z + (2 -root a)) <> 0 ;
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