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