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 = b3 - a3 & a2 - b2 = b4 - a4 ) )
assume for x being real number holds Polynom a1,a2,a3,a4,a5,x = Polynom b1,b2,b3,b4,b5,x ; :: thesis: ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 )
then ( ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) by Th7;
hence ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) ; :: thesis: verum