let a1, b1 be Real; :: thesis: ( ex a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) implies a1 = b1 )
assume A3: ( ex a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) ) ; :: thesis: a1 = b1
then consider a02, a03 being Real such that
A4: ( (a1 + a02) + a03 = 1 & p = ((a1 * p1) + (a02 * p2)) + (a03 * p3) ) ;
consider a2, a3 being Real such that
A5: ( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) by A3;
consider a001, a002, a003 being Real such that
A6: ( p = ((a001 * p1) + (a002 * p2)) + (a003 * p3) & (a001 + a002) + a003 = 1 & ( for b01, b02, b03 being Real st p = ((b01 * p1) + (b02 * p2)) + (b03 * p3) & (b01 + b02) + b03 = 1 holds
( b01 = a001 & b02 = a002 & b03 = a003 ) ) ) by A1, Th60;
( a1 = a001 & a02 = a002 & a03 = a003 ) by A4, A6;
hence a1 = b1 by A5, A6; :: thesis: verum