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 x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
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 x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let V be RealLinearSpace; :: thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let Affv be finite affinely-independent Subset of V; :: thesis: for EV being Enumeration of Affv st x in Affin Affv holds
( x in Affin (EV .: (Seg k)) iff x |-- EV = ((x |-- EV) | k) ^ (((card Affv) -' k) |-> 0) )
let E be Enumeration of Affv; :: thesis: ( x in Affin Affv implies ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ) )
set B = E .: (Seg k);
set cA = card Affv;
set cAk = (card Affv) -' k;
set xE = x |-- E;
set xEk = (x |-- E) | k;
set cAk0 = ((card Affv) -' k) |-> 0;
A1: E .: (Seg k) c= rng E by RELAT_1:111;
assume A2: x in Affin Affv ; :: thesis: ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) )
then reconsider v = x as Element of V ;
A3: len (x |-- E) = card Affv by Th16;
A4: rng E = Affv by Def1;
then A5: len E = card Affv by FINSEQ_4:62;

per cases ( k > card Affv or k <= card Affv ) ;

suppose A6: k > card Affv ; :: thesis: ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) )

then Seg (card Affv) c= Seg k by FINSEQ_1:5;
then dom E c= Seg k by A5, FINSEQ_1:def 3;
then (dom E) /\ (Seg k) = dom E by XBOOLE_1:28;
then A7: E .: (Seg k) = E .: (dom E) by RELAT_1:112;
(card Affv) - k < 0 by A6, XREAL_1:49;
then (card Affv) -' k = 0 by XREAL_0:def 2;
then A8: ((card Affv) -' k) |-> 0 is empty ;
(x |-- E) | k = x |-- E by A3, A6, FINSEQ_1:58;
hence ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ) by A2, A4, A8, A7, FINSEQ_1:34, RELAT_1:113; :: thesis: verum

end;

suppose A9: k <= card Affv ; :: thesis: ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) )

A10: len (((card Affv) -' k) |-> 0) = (card Affv) -' k by CARD_1:def 7;
A11: len ((x |-- E) | k) = k by A3, A9, FINSEQ_1:59;
(card Affv) -' k = (card Affv) - k by A9, XREAL_1:233;
then A12: len (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) = k + ((card Affv) - k) by A11, A10, FINSEQ_1:22;

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

assume A13: x in Affin (E .: (Seg k)) ; :: thesis: x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)

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

let i be Nat; :: thesis: ( 1 <= i & i <= len (x |-- E) implies (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b₁ = (x |-- E) . b₁ )
assume A14: ( 1 <= i & i <= len (x |-- E) ) ; :: thesis: (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b₁ = (x |-- E) . b₁
then A15: i in dom (x |-- E) by FINSEQ_3:25;
A16: i in dom E by A3, A5, A14, FINSEQ_3:25;
A17: i in dom (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) by A3, A12, A14, FINSEQ_3:25;

per cases ( i in dom ((x |-- E) | k) or ex n being Nat st
( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) ) by A11, A17, FINSEQ_1:25;

suppose A18: i in dom ((x |-- E) | k) ; :: thesis: (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b₁ = (x |-- E) . b₁

hence (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i = ((x |-- E) | k) . i by FINSEQ_1:def 7
.= (x |-- E) . i by A18, FUNCT_1:47 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) ; :: thesis: (x |-- E) . b₁ = (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b₁

then consider n being Nat such that
A19: n in dom (((card Affv) -' k) |-> 0) and
A20: i = k + n ;
A21: not E . i in E .: (Seg k)

proof

assume E . i in E .: (Seg k) ; :: thesis: contradiction
then consider t being object such that
A22: ( t in dom E & t in Seg k & E . t = E . i ) by FUNCT_1:def 6;
i in Seg k by A16, A22, FUNCT_1:def 4;
then A23: i <= k by FINSEQ_1:1;
i >= k by A20, NAT_1:11;
then i = k by A23, XXREAL_0:1;
hence contradiction by A19, A20, FINSEQ_3:25; :: thesis: verum

end;

(((card Affv) -' k) |-> 0) . n = 0 ;
then (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i = 0 by A11, A19, A20, FINSEQ_1:def 7;
hence (x |-- E) . i = (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i by A2, A1, A4, A13, A15, A21, Th20; :: thesis: verum

end;

end;

end;

hence x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) by A12, Th16; :: thesis: verum

end;

assume A24: x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ; :: thesis: x in Affin (E .: (Seg k))
A25: dom (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) = dom (x |-- E) by A3, A12, FINSEQ_3:29;

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

let y be set ; :: thesis: ( y in dom (x |-- E) & not E . y in E .: (Seg k) implies (x |-- E) . y = 0 )
assume that
A26: y in dom (x |-- E) and
A27: not E . y in E .: (Seg k) ; :: thesis: (x |-- E) . y = 0
reconsider i = y as Nat by A26;
i in dom E by A3, A5, A26, FINSEQ_3:29;
then not i in Seg k by A27, FUNCT_1:def 6;
then not i in dom ((x |-- E) | k) by A11, FINSEQ_1:def 3;
then consider n being Nat such that
A28: ( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) by A11, A25, A26, FINSEQ_1:25;
(((card Affv) -' k) |-> 0) . n = 0 ;
hence (x |-- E) . y = 0 by A11, A24, A28, FINSEQ_1:def 7; :: thesis: verum

end;

hence x in Affin (E .: (Seg k)) by A2, A1, A4, Th20; :: thesis: verum

end;

end;