let z be complex number ; :: thesis: z |^ 2 = z * z
z |^ (1 + 1) = (z |^ 1) * z by NEWTON:6
.= z * z by NEWTON:5 ;
hence z |^ 2 = z * z ; :: thesis: verum