let n be Nat; :: thesis: for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Cn = (r * An) + ((1 - r) * Bn) & r = 1 holds
Cn = An
let r be Real; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) st Cn = (r * An) + ((1 - r) * Bn) & r = 1 holds
Cn = An
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: ( Cn = (r * An) + ((1 - r) * Bn) & r = 1 implies Cn = An )
assume that
A1: Cn = (r * An) + ((1 - r) * Bn) and
A2: r = 1 ; :: thesis: Cn = An
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
rC = rA + (0 * rB) by A1, A2, EUCLID_4:3;
then rC = rA + (0* n) by EUCLID_4:3;
hence Cn = An by EUCLID_4:1; :: thesis: verum