let a3, b3 be Real; :: thesis: ( ex a1, a2 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a1, a2 being Real st
( (a1 + a2) + b3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b3 * p3) ) implies a3 = b3 )
assume that
A2: ex a1, a2 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) and
A3: ex a1, a2 being Real st
( (a1 + a2) + b3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b3 * p3) ) ; :: thesis: a3 = b3
consider a001, a002, a003 being Real such that
p = ((a001 * p1) + (a002 * p2)) + (a003 * p3) and
(a001 + a002) + a003 = 1 and
A4: 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, Th51;
a3 = a003 by A2, A4;
hence a3 = b3 by A3, A4; :: thesis: verum