A1: (- 2) |^ 3 = ((- 2) ^2 ) * (- 2) by Th4
.= - (4 * 2) ;
A2: (- 2) |^ 4 = 16 by Lm1, POWER:1, POWER:70;
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 ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) )
assume A3: for x being real number 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:69, POWER:70; :: thesis: verum