let n be Nat; :: thesis: for A being Subset of (REAL n)
for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st
( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds
0* n in plane (x1,x2,x3)
let A be Subset of (REAL n); :: thesis: for x, x1, x2, x3 being Element of REAL n st x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st
( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) holds
0* n in plane (x1,x2,x3)
let x, x1, x2, x3 be Element of REAL n; :: thesis: ( x in plane (x1,x2,x3) & ex c1, c2, c3 being Real st
( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) implies 0* n in plane (x1,x2,x3) )
assume that
A1: x in plane (x1,x2,x3) and
A2: ex c1, c2, c3 being Real st
( (c1 + c2) + c3 = 0 & x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) ) ; :: thesis: 0* n in plane (x1,x2,x3)
consider c1, c2, c3 being Real such that
A3: (c1 + c2) + c3 = 0 and
A4: x = ((c1 * x1) + (c2 * x2)) + (c3 * x3) by A2;
ex x9 being Element of REAL n st
( x = x9 & ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x9 = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) ) by A1;
then consider a1, a2, a3 being Real such that
A5: (a1 + a2) + a3 = 1 and
A6: x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ;
A7: ((a1 + (- c1)) + (a2 + (- c2))) + (a3 + (- c3)) = 1 by A5, A3;
0* n = x - x by Th2
.= (((a1 * x1) + (a2 * x2)) + (a3 * x3)) + ((((- c1) * x1) + ((- c2) * x2)) + ((- c3) * x3)) by A6, A4, Th14
.= (((a1 + (- c1)) * x1) + ((a2 + (- c2)) * x2)) + ((a3 + (- c3)) * x3) by Th24 ;
hence 0* n in plane (x1,x2,x3) by A7; :: thesis: verum