let a be Real; :: thesis: for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L holds
ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) )
let n be Nat; :: thesis: for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L holds
ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) )
let x1, x2 be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L holds
ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) )
let L be Element of line_of_REAL n; :: thesis: ( x1 in L & x2 in L implies ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) ) )
set x3 = ((1 - a) * x1) + (a * x2);
assume ( x1 in L & x2 in L ) ; :: thesis: ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) )
then A1: Line (x1,x2) c= L by Th48;
((1 - a) * x1) + (a * x2) = ((1 * x1) + (- (a * x1))) + (a * x2) by Th11
.= (x1 + (- (a * x1))) + (a * x2) by EUCLID_4:3
.= x1 + ((a * x2) + (- (a * x1))) by RVSUM_1:15
.= x1 + (a * (x2 - x1)) by Th12 ;
then ( ((1 - a) * x1) + (a * x2) in Line (x1,x2) & (((1 - a) * x1) + (a * x2)) - x1 = a * (x2 - x1) ) by Th6;
hence ex x3 being Element of REAL n st
( x3 in L & x3 - x1 = a * (x2 - x1) ) by A1; :: thesis: verum