theorem Th26: :: POLYEQ_5:26

for a0, a1, a2, a3 being Complex holds (((1_root_of_quartic (a0,a1,a2,a3)) + (2_root_of_quartic (a0,a1,a2,a3))) + (3_root_of_quartic (a0,a1,a2,a3))) + (4_root_of_quartic (a0,a1,a2,a3)) = - a3