let n be Nat; :: thesis: for r being Real
for An, Bn, Cn being Point of (TOP-REAL n) st An <> Bn & Cn = (r * An) + ((1 - r) * Bn) & Cn = Bn holds
r = 0
let r be Real; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) st An <> Bn & Cn = (r * An) + ((1 - r) * Bn) & Cn = Bn holds
r = 0
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: ( An <> Bn & Cn = (r * An) + ((1 - r) * Bn) & Cn = Bn implies r = 0 )
assume that
A1: An <> Bn and
A2: Cn = (r * An) + ((1 - r) * Bn) and
A3: Cn = Bn ; :: thesis: r = 0
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
rC = (r * rA) + ((1 * rB) - (r * rB)) by A2, EUCLIDLP:11
.= ((r * rA) + (- (r * rB))) + (1 * rB) by RVSUM_1:15
.= ((r * rA) - (r * rB)) + (1 * rB) ;
then (0* n) + rB = ((r * rA) - (r * rB)) + (1 * rB) by A3, EUCLID_4:1
.= ((r * rA) - (r * rB)) + rB by EUCLID_4:3 ;
then 0* n = (r * rA) - (r * rB) by RVSUM_1:25;
then r * (rA - rB) = 0* n by EUCLIDLP:12;
then ( r = 0 or rA - rB = 0* n ) by EUCLID_4:5;
hence r = 0 by A1, EUCLIDLP:9; :: thesis: verum