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;

then A13: (x |-- E) | k = k |-> 0 by A2, FINSEQ_1:33;

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

end;now :: thesis: for i being Nat st 1 <= i & i <= k holds

((x |-- E) | k) . i = (k |-> 0) . i

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

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

hence
x in Affin (Affv \ (E .: (Seg k)))
by A9, A1, Th20; :: thesis: verum(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;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