let a, b, c be Real; :: thesis: for z, z1, z2 being complex number st a <> 0 & ( for z being complex number 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 number ; :: thesis: ( a <> 0 & ( for z being complex number 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 number 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 number holds Polynom a,b,c,z = Quard a,z1,z2,z ; :: thesis: ( b / a = - (z1 + z2) & c / a = z1 * z2 )
A3: Polynom a,b,c,0 = Quard a,z1,z2,0 by A2;
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:204; :: thesis: verum