theorem Th29: :: POLYEQ_5:29

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)) = a0