:: POLYEQ_5 semantic presentation

begin


theorem Th1: :: POLYEQ_5:1
for a being complex number holds a * a = a |^ 2
proof
let a be complex number ; ::_thesis: a * a = a |^ 2
thus a * a = (a |^ 1) * a by NEWTON:5;
end;