let x be set ; ( x = Polynom a,b,c,d,z iff x = (((a * (z ^3 )) + (b * (z ^2 ))) + (c * z)) + d )
Polynom a,b,c,d,z =
(((a * (z |^ (2 + 1))) + (b * (z ^2 ))) + (c * z)) + d
.=
(((a * ((z |^ 2) * z)) + (b * (z ^2 ))) + (c * z)) + d
by NEWTON:11
;
hence
( x = Polynom a,b,c,d,z iff x = (((a * (z ^3 )) + (b * (z ^2 ))) + (c * z)) + d )
by Lm1; verum