let w1, w2 be R_eal; :: thesis: for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds

(p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2)

let wr1, wr2, p1, p2 be Real; :: thesis: ( w1 = wr1 & w2 = wr2 implies (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2) )

assume that

A1: w1 = wr1 and

A2: w2 = wr2 ; :: thesis: (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2)

A3: p2 * wr2 = p2 * w2 by A2, EXTREAL1:1;

p1 * wr1 = p1 * w1 by A1, EXTREAL1:1;

hence (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2) by A3, SUPINF_2:1; :: thesis: verum

(p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2)

let wr1, wr2, p1, p2 be Real; :: thesis: ( w1 = wr1 & w2 = wr2 implies (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2) )

assume that

A1: w1 = wr1 and

A2: w2 = wr2 ; :: thesis: (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2)

A3: p2 * wr2 = p2 * w2 by A2, EXTREAL1:1;

p1 * wr1 = p1 * w1 by A1, EXTREAL1:1;

hence (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2) by A3, SUPINF_2:1; :: thesis: verum