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