let x be set ; :: thesis: 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) )
let k be Nat; :: thesis: 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) )
let V be RealLinearSpace; :: thesis: 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) )
let Affv be finite affinely-independent Subset of V; :: thesis: 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) )
let E be Enumeration of Affv; :: thesis: ( k <= card Affv & x in Affin Affv implies ( x in Affin (Affv \ (E .: (Seg k))) iff x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) ) )
set cA = card Affv;
set B = E .: (Seg k);
set AB = Affv \ (E .: (Seg k));
set xE = x |-- E;
set xEk = (x |-- E) | k;
set xA = x |-- Affv;
set k0 = k |-> 0;
A1: Affv \ (E .: (Seg k)) c= Affv by XBOOLE_1:36;
A2: x |-- E = ((x |-- E) | k) ^ ((x |-- E) /^ k) by RFINSEQ:8;
assume A3: k <= card Affv ; :: thesis: ( not x in Affin Affv or ( x in Affin (Affv \ (E .: (Seg k))) iff x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) ) )
then A4: Seg k c= Seg (card Affv) by FINSEQ_1:5;
A5: len (x |-- E) = card Affv by Th16;
then A6: Seg (card Affv) = dom (x |-- E) by FINSEQ_1:def 3;
A7: rng E = Affv by Def1;
then len E = card Affv by FINSEQ_4:62;
then A8: dom E = dom (x |-- E) by A5, FINSEQ_3:29;
assume A9: x in Affin Affv ; :: thesis: ( x in Affin (Affv \ (E .: (Seg k))) iff x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) )
A10: ( len (k |-> 0) = k & len ((x |-- E) | k) = k ) by A3, A5, CARD_1:def 7, FINSEQ_1:59;

hereby :: thesis: ( x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) implies x in Affin (Affv \ (E .: (Seg k))) )

assume A11: x in Affin (Affv \ (E .: (Seg k))) ; :: thesis: x |-- E = (k |-> 0) ^ ((x |-- E) /^ k)

now :: thesis: for i being Nat st 1 <= i & i <= k holds
((x |-- E) | k) . i = (k |-> 0) . i

let i be Nat; :: thesis: ( 1 <= i & i <= k implies ((x |-- E) | k) . i = (k |-> 0) . i )
assume ( 1 <= i & i <= k ) ; :: thesis: ((x |-- E) | k) . i = (k |-> 0) . i
then A12: i in Seg k ;
then E . i in E .: (Seg k) by A8, A4, A6, FUNCT_1:def 6;
then not E . i in Affv \ (E .: (Seg k)) by XBOOLE_0:def 5;
then (x |-- E) . i = 0 by A9, A1, A4, A6, A11, A12, Th20;
hence ((x |-- E) | k) . i = (k |-> 0) . i by A12, FUNCT_1:49; :: thesis: verum

end;

hence x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) by A10, A2, FINSEQ_1:14; :: thesis: verum

end;

assume x |-- E = (k |-> 0) ^ ((x |-- E) /^ k) ; :: thesis: x in Affin (Affv \ (E .: (Seg k)))
then A13: (x |-- E) | k = k |-> 0 by A2, FINSEQ_1:33;

now :: thesis: for y being set st y in dom (x |-- E) & not E . y in Affv \ (E .: (Seg k)) holds
(x |-- E) . y = 0

let y be set ; :: thesis: ( y in dom (x |-- E) & not E . y in Affv \ (E .: (Seg k)) implies (x |-- E) . y = 0 )
assume that
A14: y in dom (x |-- E) and
A15: not E . y in Affv \ (E .: (Seg k)) ; :: thesis: (x |-- E) . y = 0
E . y in Affv by A7, A8, A14, FUNCT_1:def 3;
then E . y in E .: (Seg k) by A15, XBOOLE_0:def 5;
then consider z being object such that
A16: z in dom E and
A17: z in Seg k and
A18: E . z = E . y by FUNCT_1:def 6;
z = y by A8, A14, A16, A18, FUNCT_1:def 4;
then ((x |-- E) | k) . y = (x |-- E) . y by A17, FUNCT_1:49;
hence (x |-- E) . y = 0 by A13; :: thesis: verum

end;

hence x in Affin (Affv \ (E .: (Seg k))) by A9, A1, Th20; :: thesis: verum