theorem Th18: :: POLYEQ_5:18

for a0, a1, a2 being Complex holds (((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) = a1