let a, a9, b, b9, c, c9, d, d9 be Real; :: thesis: ( ( for x being Real holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) implies ( a = a9 & b = b9 & c = c9 & d = d9 ) )
(- 1) |^ 3 = - (1 |^ (2 + 1)) by Lm1, POWER:2
.= - ((1 |^ 2) * 1) by NEWTON:6 ;
then A1: ( 0 |^ 3 = 0 & (- 1) |^ 3 = - 1 ) by NEWTON:10, NEWTON:11;
A2: 2 |^ 1 = 2 to_power 1 by POWER:41
.= 2 by POWER:25 ;
A3: 2 |^ 3 = 2 |^ (2 + 1)
.= (2 |^ (1 + 1)) * 2 by NEWTON:6
.= ((2 |^ 1) * 2) * 2 by NEWTON:6
.= (2 |^ 1) * (2 * 2) ;
assume A4: for x being Real holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ; :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 )
then A5: Polynom (a,b,c,d,2) = Polynom (a9,b9,c9,d9,2) ;
Polynom (a,b,c,d,1) = Polynom (a9,b9,c9,d9,1) by A4;
then (((a * 1) + (b * 1)) + (c * 1)) + d = Polynom (a9,b9,c9,d9,1) by NEWTON:10;
then A6: ((a + b) + c) + d = (((a9 * 1) + (b9 * 1)) + (c9 * 1)) + d9 by NEWTON:10
.= ((a9 + b9) + c9) + d9 ;
( Polynom (a,b,c,d,0) = Polynom (a9,b9,c9,d9,0) & Polynom (a,b,c,d,(- 1)) = Polynom (a9,b9,c9,d9,(- 1)) ) by A4;
hence ( a = a9 & b = b9 & c = c9 & d = d9 ) by A6, A1, A5, A3, A2; :: thesis: verum