let a, b, c, d, a', b', c', d' be real number ; :: thesis: ( ( for x being real number holds Polynom a,b,c,d,x = Polynom a',b',c',d',x ) implies ( a = a' & b = b' & c = c' & d = d' ) )
assume A1: for x being real number holds Polynom a,b,c,d,x = Polynom a',b',c',d',x ; :: thesis: ( a = a' & b = b' & c = c' & d = d' )
then A2: Polynom a,b,c,d,0 = Polynom a',b',c',d',0 ;
A3: 0 |^ 3 = 0 by NEWTON:16;
Polynom a,b,c,d,1 = Polynom a',b',c',d',1 by A1;
then (((a * 1) + (b * 1)) + (c * 1)) + d = Polynom a',b',c',d',1 by NEWTON:15;
then A4: ((a + b) + c) + d = (((a' * 1) + (b' * 1)) + (c' * 1)) + d' by NEWTON:15
.= ((a' + b') + c') + d' ;
A5: Polynom a,b,c,d,(- 1) = Polynom a',b',c',d',(- 1) by A1;
3 = (2 * 1) + 1 ;
then (- 1) |^ 3 = - (1 |^ (2 + 1)) by POWER:2
.= - ((1 |^ 2) * 1) by NEWTON:11 ;
then A6: (- 1) |^ 3 = - 1 by NEWTON:15;
A7: Polynom a,b,c,d,2 = Polynom a',b',c',d',2 by A1;
A8: 2 |^ 3 = 2 |^ (2 + 1)
.= (2 |^ (1 + 1)) * 2 by NEWTON:11
.= ((2 |^ 1) * 2) * 2 by NEWTON:11
.= (2 |^ 1) * (2 * 2) ;
A9: 2 |^ 1 = 2 to_power 1 by POWER:46
.= 2 by POWER:30 ;
thus ( a = a' & b = b' & c = c' & d = d' ) by A2, A3, A4, A5, A6, A7, A8, A9; :: thesis: verum