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:6
;
hence
( x = Polynom (a,b,c,d,z) iff x = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d )
by Lm1; verum