theorem lemcontr2: :: FIELD_10:1

for r, s being Complex holds (r * s) |^ 3 = (r |^ 3) * (s |^ 3)