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