theorem Th22: :: RLAFFIN3:22

for x being set
for k being Nat
for V being RealLinearSpace
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st k <= card Affv & x in Affin Affv holds
( x in Affin (Affv \ (EV .: (Seg k))) iff x |-- EV = (k |-> 0) ^ ((x |-- EV) /^ k) )