ex a01, a02, a03 being Real st
( p = ((a01 * p1) + (a02 * p2)) + (a03 * p3) & (a01 + a02) + a03 = 1 & ( for b1, b2, b3 being Real st p = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a01 & b2 = a02 & b3 = a03 ) ) ) by A1, Th51;
hence ex b₁, a2, a3 being Real st
( (b₁ + a2) + a3 = 1 & p = ((b₁ * p1) + (a2 * p2)) + (a3 * p3) ) ; :: thesis: verum