let a, b, c, x be Complex; ( a <> 0 & delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 implies x = - (b / (2 * a)) )
assume that
A1:
a <> 0
and
A2:
( delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 )
; x = - (b / (2 * a))
((((2 * a) * x) + b) ^2) - 0 = 0
by A1, A2, Th14;
then A3:
((2 * a) * x) + b = 0
by XCMPLX_1:6;
2 * a <> 0
by A1;
then
x = (- b) / (2 * a)
by A3, XCMPLX_1:89;
hence
x = - (b / (2 * a))
by XCMPLX_1:187; verum