let n be Nat; for x, x1, x2, x3 being Element of REAL n holds
( x in plane (x1,x2,x3) iff ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) )
let x, x1, x2, x3 be Element of REAL n; ( x in plane (x1,x2,x3) iff ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) )
thus
( x in plane (x1,x2,x3) implies ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) )
( ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) implies x in plane (x1,x2,x3) )proof
assume
x in plane (
x1,
x2,
x3)
;
ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) )
then
ex
x9 being
Element of
REAL n st
(
x = x9 & ex
a19,
a29,
a39 being
Real st
(
(a19 + a29) + a39 = 1 &
x9 = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ) )
;
hence
ex
a1,
a2,
a3 being
Real st
(
(a1 + a2) + a3 = 1 &
x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) )
;
verum
end;
thus
( ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) ) implies x in plane (x1,x2,x3) )
; verum