let a, b, c be Real; for z, z1, z2 being Complex st a <> 0 & ( for z being Complex holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ) holds
( b / a = - (z1 + z2) & c / a = z1 * z2 )
let z, z1, z2 be Complex; ( a <> 0 & ( for z being Complex holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ) implies ( b / a = - (z1 + z2) & c / a = z1 * z2 ) )
assume A1:
a <> 0
; ( ex z being Complex st not Polynom (a,b,c,z) = Quard (a,z1,z2,z) or ( b / a = - (z1 + z2) & c / a = z1 * z2 ) )
assume A2:
for z being Complex holds Polynom (a,b,c,z) = Quard (a,z1,z2,z)
; ( b / a = - (z1 + z2) & c / a = z1 * z2 )
then A3:
Polynom (a,b,c,0) = Quard (a,z1,z2,0)
;
Quard (a,z1,z2,1) =
Polynom (a,b,c,1)
by A2
.=
(a + b) + c
;
then
(a + b) + c = (a + (a * (- (z1 + z2)))) + c
by A3;
hence
( b / a = - (z1 + z2) & c / a = z1 * z2 )
by A1, A3, XCMPLX_1:203; verum