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