let b, c be Real; for z being Complex st b <> 0 & ( for z being Complex holds Polynom (0,b,c,z) = 0 ) holds
z = - (c / b)
let z be Complex; ( b <> 0 & ( for z being Complex holds Polynom (0,b,c,z) = 0 ) implies z = - (c / b) )
A1:
0 = 0 + (0 * <i>)
;
assume A2:
b <> 0
; ( ex z being Complex st not Polynom (0,b,c,z) = 0 or z = - (c / b) )
assume A3:
for z being Complex holds Polynom (0,b,c,z) = 0
; z = - (c / b)
hence
z = - (c / b)
; verum