A1: (- 2) |^ 3 = ((- 2) ^2) * (- 2) by Th4
.= - (4 * 2) ;
A2: (- 2) |^ 4 = 16 by Lm1, POWER:1, POWER:62;
let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be Real; :: thesis: ( ( for x being Real holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) )
assume A3: for x being Real holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; :: thesis: ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 )
then A4: Polynom (a1,a2,a3,a4,a5,(- 2)) = Polynom (b1,b2,b3,b4,b5,(- 2)) ;
A5: ( a5 = b5 & Polynom (a1,a2,a3,a4,a5,2) = Polynom (b1,b2,b3,b4,b5,2) ) by A3, Th7;
( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) by A3, Th8;
hence ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) by A5, A4, A2, A1, POWER:61, POWER:62; :: thesis: verum