let a2, a3 be Real; :: thesis: for n being Nat
for x, x1, x2, x3 being Element of REAL n st x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds
ex a1 being Real st
( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 )
let n be Nat; :: thesis: for x, x1, x2, x3 being Element of REAL n st x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) holds
ex a1 being Real st
( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 )
let x, x1, x2, x3 be Element of REAL n; :: thesis: ( x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) implies ex a1 being Real st
( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) )
assume A1: x = (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) ; :: thesis: ex a1 being Real st
( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 )
reconsider a1 = (1 - a2) - a3 as Real ;
take a1 ; :: thesis: ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 )
((a1 * x1) + (a2 * x2)) + (a3 * x3) = ((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by Th13
.= (((x1 + (- (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by EUCLID_4:3
.= (((x1 + (- (a2 * x1))) + (a2 * x2)) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15
.= ((x1 + ((a2 * x2) + (- (a2 * x1)))) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:15
.= (x1 + ((a2 * x2) + (- (a2 * x1)))) + ((a3 * x3) + (- (a3 * x1))) by RVSUM_1:15
.= (x1 + (a2 * (x2 - x1))) + ((a3 * x3) + (- (a3 * x1))) by Th12
.= x by A1, Th12 ;
hence ( x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (a1 + a2) + a3 = 1 ) ; :: thesis: verum