theorem Th8: :: NUMBER17:8

for c1, c2 being Complex holds <*c1,c2*> ^2 = <*(c1 ^2),(c2 ^2)*>