let w1, w2 be R_eal; 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; ( w1 = wr1 & w2 = wr2 implies (p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2) )
assume that
A1:
w1 = wr1
and
A2:
w2 = wr2
; (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; verum