let a, b, c be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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) ; :: thesis: ( 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; :: thesis: verum