let a0, a1, a2 be Complex; :: thesis: ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2

per cases ( (3 * a1) - (a2 |^ 2) = 0 or (3 * a1) - (a2 |^ 2) <> 0 ) ;

suppose A1: (3 * a1) - (a2 |^ 2) = 0 ; :: thesis: ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2

then A2: ex r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & 3_root_of_cubic (a0,a1,a2) = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i>) / 2) ) by Def4;
( ex r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & 1_root_of_cubic (a0,a1,a2) = s1 - (a2 / 3) ) & ex r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & 2_root_of_cubic (a0,a1,a2) = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i>) / 2) ) ) by A1, Def2, Def3;
hence ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2 by A2; :: thesis: verum

end;

suppose A3: (3 * a1) - (a2 |^ 2) <> 0 ; :: thesis: ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2

then A4: ex q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & 3_root_of_cubic (a0,a1,a2) = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) by Def4;
( ex q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & 1_root_of_cubic (a0,a1,a2) = (s1 + s2) - (a2 / 3) ) & ex q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & 2_root_of_cubic (a0,a1,a2) = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) by A3, Def2, Def3;
hence ((1_root_of_cubic (a0,a1,a2)) + (2_root_of_cubic (a0,a1,a2))) + (3_root_of_cubic (a0,a1,a2)) = - a2 by A4; :: thesis: verum

end;

end;