let n be Element of NAT ; :: thesis: for p1, p2, p3, p0 being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p0 in plane p1,p2,p3 holds
ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )
let p1, p2, p3, p0 be Point of (TOP-REAL n); :: thesis: ( p2 - p1,p3 - p1 are_lindependent2 & p0 in plane p1,p2,p3 implies ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) ) )
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 & p0 in plane p1,p2,p3 ) ; :: thesis: ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )
set q2 = p2 - p1;
set q3 = p3 - p1;
consider a01, a02, a03 being Real such that
A2: ( (a01 + a02) + a03 = 1 & p0 = ((a01 * p1) + (a02 * p2)) + (a03 * p3) ) by A1, Th57;
for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a01 & b2 = a02 & b3 = a03 )

proof

let b1, b2, b3 be Real; :: thesis: ( p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 implies ( b1 = a01 & b2 = a02 & b3 = a03 ) )
assume A3: ( p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 ) ; :: thesis: ( b1 = a01 & b2 = a02 & b3 = a03 )
then A4: p0 + (- p1) = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 + b2) + b3) * p1)) by EUCLID:33
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 + b2) * p1) + (b3 * p1))) by EUCLID:37
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 * p1) + (b2 * p1)) + (b3 * p1))) by EUCLID:37
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ((- ((b1 * p1) + (b2 * p1))) - (b3 * p1)) by EUCLID:42
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (((- (b1 * p1)) - (b2 * p1)) - (b3 * p1)) by EUCLID:42
.= ((b1 * p1) + ((b2 * p2) + (b3 * p3))) + (((- (b1 * p1)) + (- (b2 * p1))) + (- (b3 * p1))) by EUCLID:30
.= ((b1 * p1) + ((b2 * p2) + (b3 * p3))) + ((- (b1 * p1)) + ((- (b2 * p1)) + (- (b3 * p1)))) by EUCLID:30
.= ((((b2 * p2) + (b3 * p3)) + (b1 * p1)) - (b1 * p1)) + ((- (b2 * p1)) + (- (b3 * p1))) by EUCLID:30
.= ((b2 * p2) + (b3 * p3)) + ((- (b2 * p1)) + (- (b3 * p1))) by EUCLID:52
.= (((b2 * p2) + (b3 * p3)) + (- (b2 * p1))) + (- (b3 * p1)) by EUCLID:30
.= (((b2 * p2) + (- (b2 * p1))) + (b3 * p3)) + (- (b3 * p1)) by EUCLID:30
.= (((b2 * p2) + (b2 * (- p1))) + (b3 * p3)) + (- (b3 * p1)) by EUCLID:44
.= ((b2 * (p2 + (- p1))) + (b3 * p3)) + (- (b3 * p1)) by EUCLID:36
.= (b2 * (p2 + (- p1))) + ((b3 * p3) + (- (b3 * p1))) by EUCLID:30
.= (b2 * (p2 + (- p1))) + ((b3 * p3) + (b3 * (- p1))) by EUCLID:44
.= (b2 * (p2 - p1)) + (b3 * (p3 - p1)) by EUCLID:36 ;
p0 + (- p1) = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 + a02) + a03) * p1)) by A2, EUCLID:33
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 + a02) * p1) + (a03 * p1))) by EUCLID:37
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 * p1) + (a02 * p1)) + (a03 * p1))) by EUCLID:37
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ((- ((a01 * p1) + (a02 * p1))) - (a03 * p1)) by EUCLID:42
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (((- (a01 * p1)) - (a02 * p1)) - (a03 * p1)) by EUCLID:42
.= ((a01 * p1) + ((a02 * p2) + (a03 * p3))) + (((- (a01 * p1)) + (- (a02 * p1))) + (- (a03 * p1))) by EUCLID:30
.= ((a01 * p1) + ((a02 * p2) + (a03 * p3))) + ((- (a01 * p1)) + ((- (a02 * p1)) + (- (a03 * p1)))) by EUCLID:30
.= ((((a02 * p2) + (a03 * p3)) + (a01 * p1)) - (a01 * p1)) + ((- (a02 * p1)) + (- (a03 * p1))) by EUCLID:30
.= ((a02 * p2) + (a03 * p3)) + ((- (a02 * p1)) + (- (a03 * p1))) by EUCLID:52
.= (((a02 * p2) + (a03 * p3)) + (- (a02 * p1))) + (- (a03 * p1)) by EUCLID:30
.= (((a02 * p2) + (- (a02 * p1))) + (a03 * p3)) + (- (a03 * p1)) by EUCLID:30
.= (((a02 * p2) + (a02 * (- p1))) + (a03 * p3)) + (- (a03 * p1)) by EUCLID:44
.= ((a02 * (p2 + (- p1))) + (a03 * p3)) + (- (a03 * p1)) by EUCLID:36
.= (a02 * (p2 + (- p1))) + ((a03 * p3) + (- (a03 * p1))) by EUCLID:30
.= (a02 * (p2 + (- p1))) + ((a03 * p3) + (a03 * (- p1))) by EUCLID:44
.= (a02 * (p2 - p1)) + (a03 * (p3 - p1)) by EUCLID:36 ;
then ((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + (- ((a02 * (p2 - p1)) + (a03 * (p3 - p1)))) = 0. (TOP-REAL n) by A4, EUCLID:40;
then ((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + ((- (a02 * (p2 - p1))) - (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:42;
then (((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + (- (a02 * (p2 - p1)))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:30;
then (((b2 * (p2 - p1)) + (- (a02 * (p2 - p1)))) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:30;
then (((b2 * (p2 - p1)) + ((- a02) * (p2 - p1))) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:44;
then (((b2 + (- a02)) * (p2 - p1)) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:37;
then ((b2 + (- a02)) * (p2 - p1)) + ((b3 * (p3 - p1)) + (- (a03 * (p3 - p1)))) = 0. (TOP-REAL n) by EUCLID:30;
then ((b2 + (- a02)) * (p2 - p1)) + ((b3 * (p3 - p1)) + ((- a03) * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:44;
then ((b2 + (- a02)) * (p2 - p1)) + ((b3 + (- a03)) * (p3 - p1)) = 0. (TOP-REAL n) by EUCLID:37;
then ( (b2 - a02) + a02 = 0 + a02 & b3 + (- a03) = 0 ) by A1, Def10;
hence ( b1 = a01 & b2 = a02 & b3 = a03 ) by A2, A3; :: thesis: verum

end;

hence ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) ) by A2; :: thesis: verum