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