:: 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;