theorem Th12: :: TOPREALC:12

for x being object
for n being Nat
for c being Complex holds ((0* n) +* (x,c)) ^2 = (0* n) +* (x,(c ^2))