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 A3, FINSEQ_3:29;
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 A1, RLAFFIN1:77;
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 A8, FUNCT_1:11;
then EV . y in Affv by A4, FUNCT_1:def 3;
then reconsider Ey = EV . y as Element of V ;
( (x |-- EV) . y = (x |-- Affv) . (EV . y) & not Ey in Carrier (x |-- B) ) by A6, A8, A9, FUNCT_1:12;
hence (x |-- EV) . y = 0 by A7, RLVECT_2:19; :: 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 A4, FUNCT_1:def 3;
not y in B by A12, XBOOLE_0:def 5;
then (x |-- EV) . z = 0 by A5, A10, A13;
hence (x |-- Affv) . y = 0 by A5, A13, FUNCT_1:12; :: thesis: verum

end;

Affv \ (Affv \ B) = Affv /\ B by XBOOLE_1:48
.= B by A1, XBOOLE_1:28 ;
hence x in Affin B by A2, A11, RLAFFIN1:75; :: thesis: verum