set x = - 1;
let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; :: thesis: ( ( for x being real number holds Polynom a1,a2,a3,a4,a5,x = Polynom b1,b2,b3,b4,b5,x ) implies ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) )
A1: ( 0 |^ 3 = 0 & 0 |^ 4 = 0 ) by NEWTON:16;
assume A2: for x being real number holds Polynom a1,a2,a3,a4,a5,x = Polynom b1,b2,b3,b4,b5,x ; :: thesis: ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 )
then A3: Polynom a1,a2,a3,a4,a5,(- 1) = Polynom b1,b2,b3,b4,b5,(- 1) ;
A4: ( 1 |^ 3 = 1 & 1 |^ 4 = 1 ) by NEWTON:15;
A5: ( (- 1) |^ 3 = ((- 1) ^2 ) * (- 1) & ((- 1) |^ 3) * (- 1) = (- 1) |^ 4 ) by Th4;
( Polynom a1,a2,a3,a4,a5,0 = Polynom b1,b2,b3,b4,b5,0 & Polynom a1,a2,a3,a4,a5,1 = Polynom b1,b2,b3,b4,b5,1 ) by A2;
hence ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) by A1, A4, A3, A5; :: thesis: verum