let a1, a2, a3 be Real; :: thesis: for n being Element of NAT
for x1, x3, x, x2 being Element of REAL n st x1 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds
0* n in plane x1,x2,x3
let n be Element of NAT ; :: thesis: for x1, x3, x, x2 being Element of REAL n st x1 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds
0* n in plane x1,x2,x3
let x1, x3, x, x2 be Element of REAL n; :: thesis: ( x1 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 implies 0* n in plane x1,x2,x3 )
assume A1: ( x1 - x1,x3 - x1 are_lindependent2 & x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 ) ; :: thesis: 0* n in plane x1,x2,x3
then consider x' being Element of REAL n such that
A2: ( x = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * x1) + (a2' * x2)) + (a3' * x3) ) ) ;
consider a1', a2', a3' being Real such that
A3: ( (a1' + a2') + a3' = 1 & x = ((a1' * x1) + (a2' * x2)) + (a3' * x3) ) by A2;
A4: 0* n = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((a1' * x1) + (a2' * x2)) + (a3' * x3)) by A1, A3, Th7
.= (((a1 - a1') * x1) + ((a2 - a2') * x2)) + ((a3 - a3') * x3) by Th31 ;
A5: ((a1 - a1') + (a2 - a2')) + (a3 - a3') <> 0 by A1, A3;
set t = ((a1 - a1') + (a2 - a2')) + (a3 - a3');
A6: 0* n = (1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (0* n) by EUCLID_4:2
.= ((((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a1 - a1')) * x1) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a2 - a2')) * x2)) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a3 - a3')) * x3) by A4, Th27
.= ((((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x1) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a2 - a2')) * x2)) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a3 - a3')) * x3) by XCMPLX_1:100
.= ((((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x1) + (((a2 - a2') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x2)) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a3 - a3')) * x3) by XCMPLX_1:100
.= ((((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x1) + (((a2 - a2') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x2)) + (((a3 - a3') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x3) by XCMPLX_1:100 ;
(((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) + ((a2 - a2') / (((a1 - a1') + (a2 - a2')) + (a3 - a3')))) + ((a3 - a3') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) = (((a1 - a1') + (a2 - a2')) + (a3 - a3')) / (((a1 - a1') + (a2 - a2')) + (a3 - a3')) by XCMPLX_1:64
.= 1 by A5, XCMPLX_1:60 ;
hence 0* n in plane x1,x2,x3 by A6; :: thesis: verum