let x1, x2 be Real; :: thesis: for a, b, c being Complex st a <> 0 & ( for x being Real holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds
( b / a = - (x1 + x2) & c / a = x1 * x2 )
let a, b, c be Complex; :: thesis: ( a <> 0 & ( for x being Real holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) implies ( b / a = - (x1 + x2) & c / a = x1 * x2 ) )
assume A1: a <> 0 ; :: thesis: ( ex x being Real st not Polynom (a,b,c,x) = Quard (a,x1,x2,x) or ( b / a = - (x1 + x2) & c / a = x1 * x2 ) )
assume A2: for x being Real holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ; :: thesis: ( b / a = - (x1 + x2) & c / a = x1 * x2 )

now :: thesis: for z being Real holds Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z)

let z be Real; :: thesis: Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z)
set h = z - x1;
set t = z - x2;
set e = ((z - x1) * (z - x2)) - (z ^2);
Polynom (a,b,c,z) = Quard (a,x1,x2,z) by A2;
then a * (((z - x1) * (z - x2)) - (z ^2)) = (b * z) + c ;
then ((z - x1) * (z - x2)) - (z ^2) = ((b * z) + c) / a by A1, XCMPLX_1:89
.= (a ") * ((b * z) + c) by XCMPLX_0:def 9
.= ((a ") * (b * z)) + ((a ") * c) ;
then (((z * z) - (z * x2)) - (x1 * z)) + (x1 * x2) = ((z ^2) + (((a ") * b) * z)) + ((a ") * c) ;
then ((z ^2) - ((x1 + x2) * z)) + (x1 * x2) = ((z ^2) + ((b / a) * z)) + ((a ") * c) by XCMPLX_0:def 9
.= ((z ^2) + ((b / a) * z)) + (c / a) by XCMPLX_0:def 9 ;
hence Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z) ; :: thesis: verum

end;

hence ( b / a = - (x1 + x2) & c / a = x1 * x2 ) by Th4; :: thesis: verum