let x be Complex; :: thesis: ( x |^ 2 = x * x & x ^2 = x |^ 2 )
thus x * x = (x |^ 1) * x
.= x |^ (1 + 1) by Th6
.= x |^ 2 ; :: thesis: x ^2 = x |^ 2
hence x ^2 = x |^ 2 ; :: thesis: verum