let a1, a2, a3, b1, b2, b3 be Real; :: thesis: for n being Element of NAT
for x2, x1, x3, x being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds
( a1 = b1 & a2 = b2 & a3 = b3 )
let n be Element of NAT ; :: thesis: for x2, x1, x3, x being Element of REAL n st x2 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) holds
( a1 = b1 & a2 = b2 & a3 = b3 )
let x2, x1, x3, x be Element of REAL n; :: thesis: ( x2 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) implies ( a1 = b1 & a2 = b2 & a3 = b3 ) )
assume A1: ( x2 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 ) ; :: thesis: ( not (a1 + a2) + a3 = 1 or not x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) or not (b1 + b2) + b3 = 1 or not x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) or ( a1 = b1 & a2 = b2 & a3 = b3 ) )
assume A2: ( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ) ; :: thesis: ( a1 = b1 & a2 = b2 & a3 = b3 )
then a1 = (1 - a2) - a3 ;
then x = ((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3) by A2, Th18
.= (((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:32
.= ((x1 + ((a2 * x2) + (- (a2 * x1)))) + (- (a3 * x1))) + (a3 * x3) by RVSUM_1:32
.= (x1 + ((a2 * x2) + (- (a2 * x1)))) + ((a3 * x3) + (- (a3 * x1))) by RVSUM_1:32
.= (x1 + ((a2 * x2) + (a2 * (- x1)))) + ((a3 * x3) + (- (a3 * x1))) by Th8
.= (x1 + ((a2 * x2) + (a2 * (- x1)))) + ((a3 * x3) + (a3 * (- x1))) by Th8
.= (x1 + (a2 * (x2 + (- x1)))) + ((a3 * x3) + (a3 * (- x1))) by EUCLID_4:6
.= (x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)) by EUCLID_4:6 ;
then A3: x - x1 = (a2 * (x2 - x1)) + (a3 * (x3 - x1)) by Th12;
x = ((((1 - b2) - b3) * x1) + (b2 * x2)) + (b3 * x3) by A2
.= ((((1 * x1) - (b2 * x1)) - (b3 * x1)) + (b2 * x2)) + (b3 * x3) by Th18
.= (((x1 + (- (b2 * x1))) - (b3 * x1)) + (b2 * x2)) + (b3 * x3) by EUCLID_4:3
.= (((x1 + (- (b2 * x1))) + (b2 * x2)) + (- (b3 * x1))) + (b3 * x3) by RVSUM_1:32
.= ((x1 + ((b2 * x2) + (- (b2 * x1)))) + (- (b3 * x1))) + (b3 * x3) by RVSUM_1:32
.= (x1 + ((b2 * x2) + (- (b2 * x1)))) + ((b3 * x3) + (- (b3 * x1))) by RVSUM_1:32
.= (x1 + ((b2 * x2) + (b2 * (- x1)))) + ((b3 * x3) + (- (b3 * x1))) by Th8
.= (x1 + ((b2 * x2) + (b2 * (- x1)))) + ((b3 * x3) + (b3 * (- x1))) by Th8
.= (x1 + (b2 * (x2 + (- x1)))) + ((b3 * x3) + (b3 * (- x1))) by EUCLID_4:6
.= (x1 + (b2 * (x2 - x1))) + (b3 * (x3 - x1)) by EUCLID_4:6 ;
then (a2 * (x2 - x1)) + (a3 * (x3 - x1)) = (b2 * (x2 - x1)) + (b3 * (x3 - x1)) by A3, Th12;
then ( a2 = b2 & a3 = b3 ) by A1, Th40;
hence ( a1 = b1 & a2 = b2 & a3 = b3 ) by A2; :: thesis: verum