let a be complex number ; :: thesis: a * a = a |^ 2
thus a * a = (a |^ 1) * a by NEWTON:10
.= a |^ (1 + 1) by NEWTON:11
.= a |^ 2 ; :: thesis: verum