let x be complex number ; :: thesis: ( x |^ 2 = x * x & x ^2 = x |^ 2 )
thus x * x = (x |^ 1) * x by Th10
.= x |^ (1 + 1) by Th11
.= x |^ 2 ; :: thesis: x ^2 = x |^ 2
hence x ^2 = x |^ 2 ; :: thesis: verum