let a, b, c be Real; for z being Complex st a <> 0 & delta (a,b,c) < 0 & Polynom (a,b,c,0,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) holds
z = 0
let z be Complex; ( a <> 0 & delta (a,b,c) < 0 & Polynom (a,b,c,0,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) implies z = 0 )
assume that
A1:
( a <> 0 & delta (a,b,c) < 0 )
and
A2:
Polynom (a,b,c,0,z) = 0
; ( z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) or z = 0 )
(((a * (z ^2)) + (b * z)) + c) * z = 0
by A2;
then
( Polynom (a,b,c,z) = 0 or z = 0 )
;
hence
( z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) or z = 0 )
by A1, Th2; verum