let x be set ; :: thesis: for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )

let V be RealLinearSpace; :: thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )

let Affv be finite affinely-independent Subset of V; :: thesis: for EV being Enumeration of Affv
for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )

let EV be Enumeration of Affv; :: thesis: for A being Subset of V st A c= Affv & x in Affin Affv holds
( x in Affin A iff for y being set st y in dom (x |-- EV) & not EV . y in A holds
(x |-- EV) . y = 0 )

let B be Subset of V; :: thesis: ( B c= Affv & x in Affin Affv implies ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ) )

assume A1: B c= Affv ; :: thesis: ( not x in Affin Affv or ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ) )

set xA = x |-- Affv;
set xB = x |-- B;
set cA = card Affv;
set E = EV;
assume A2: x in Affin Affv ; :: thesis: ( x in Affin B iff for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 )

set xE = x |-- EV;
A3: len (x |-- EV) = card Affv by Th16;
A4: rng EV = Affv by Def1;
then len EV = card Affv by FINSEQ_4:62;
then A5: dom (x |-- EV) = dom EV by ;
A6: Carrier (x |-- B) c= B by RLVECT_2:def 6;
hereby :: thesis: ( ( for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ) implies x in Affin B )
assume x in Affin B ; :: thesis: for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0

then A7: x |-- B = x |-- Affv by ;
let y be set ; :: thesis: ( y in dom (x |-- EV) & not EV . y in B implies (x |-- EV) . y = 0 )
assume that
A8: y in dom (x |-- EV) and
A9: not EV . y in B ; :: thesis: (x |-- EV) . y = 0
y in dom EV by ;
then EV . y in Affv by ;
then reconsider Ey = EV . y as Element of V ;
( (x |-- EV) . y = (x |-- Affv) . (EV . y) & not Ey in Carrier (x |-- B) ) by ;
hence (x |-- EV) . y = 0 by ; :: thesis: verum
end;
assume A10: for y being set st y in dom (x |-- EV) & not EV . y in B holds
(x |-- EV) . y = 0 ; :: thesis: x in Affin B
A11: now :: thesis: for y being set st y in Affv \ B holds
(x |-- Affv) . y = 0
let y be set ; :: thesis: ( y in Affv \ B implies (x |-- Affv) . y = 0 )
assume A12: y in Affv \ B ; :: thesis: (x |-- Affv) . y = 0
then y in Affv by XBOOLE_0:def 5;
then consider z being object such that
A13: ( z in dom EV & EV . z = y ) by ;
not y in B by ;
then (x |-- EV) . z = 0 by A5, A10, A13;
hence (x |-- Affv) . y = 0 by ; :: thesis: verum
end;
Affv \ (Affv \ B) = Affv /\ B by XBOOLE_1:48
.= B by ;
hence x in Affin B by ; :: thesis: verum