let x be set ; :: thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V
for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
let I be affinely-independent Subset of V; :: thesis: for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
let B be Subset of V; :: thesis: ( x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) implies ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) )
assume that
A1: x in Affin I and
A2: for y being set st y in B holds
(x |-- I) . y = 0 ; :: thesis: ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
A3: Affin I = { (Sum L) where L is Linear_Combination of I : sum L = 1 } by Th59;
A4: I \ B is affinely-independent by Th43, XBOOLE_1:36;
consider L being Linear_Combination of I such that
A5: ( x = Sum L & sum L = 1 ) by A1, A3;
A6: x |-- I = L by A1, A5, Def7;
Carrier L c= I \ B

proof

A7: Carrier L c= I by RLVECT_2:def 6;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Carrier L or y in I \ B )
assume A8: y in Carrier L ; :: thesis: y in I \ B
assume not y in I \ B ; :: thesis: contradiction
then y in B by A7, A8, XBOOLE_0:def 5;
then L . y = 0 by A2, A6;
hence contradiction by A8, RLVECT_2:19; :: thesis: verum

end;

then A9: L is Linear_Combination of I \ B by RLVECT_2:def 6;
then x in { (Sum K) where K is Linear_Combination of I \ B : sum K = 1 } by A5;
then x in Affin (I \ B) by Th59;
hence ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) by A4, A5, A6, A9, Def7; :: thesis: verum