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 ;
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 ;
then (card Affv) -' k = 0 by XREAL_0:def 2;
then A8: ((card Affv) -' k) |-> 0 is empty ;
(x |-- E) | k = x |-- E by ;
hence ( x in Affin (E .: (Seg k)) iff x |-- E = ((x |-- E) | k) ^ (((card Affv) -' k) |-> 0) ) by ; :: 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 ;
(card Affv) -' k = (card Affv) - k by ;
then A12: len (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) = k + ((card Affv) - k) by ;
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)) . b1 = (x |-- E) . b1 )
assume A14: ( 1 <= i & i <= len (x |-- E) ) ; :: thesis: (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1 = (x |-- E) . b1
then A15: i in dom (x |-- E) by FINSEQ_3:25;
A16: i in dom E by ;
A17: i in dom (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) by ;
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 ;
suppose A18: i in dom ((x |-- E) | k) ; :: thesis: (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1 = (x |-- E) . b1
hence (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . i = ((x |-- E) | k) . i by FINSEQ_1:def 7
.= (x |-- E) . i by ;
:: thesis: verum
end;
suppose ex n being Nat st
( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) ; :: thesis: (x |-- E) . b1 = (((x |-- E) | k) ^ (((card Affv) -' k) |-> 0)) . b1
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 ;
then A23: i <= k by FINSEQ_1:1;
i >= k by ;
then i = k by ;
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 ;
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 ; :: 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 ;
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 ;
then not i in Seg k by ;
then not i in dom ((x |-- E) | k) by ;
then consider n being Nat such that
A28: ( n in dom (((card Affv) -' k) |-> 0) & i = k + n ) by ;
(((card Affv) -' k) |-> 0) . n = 0 ;
hence (x |-- E) . y = 0 by ; :: thesis: verum
end;
hence x in Affin (E .: (Seg k)) by A2, A1, A4, Th20; :: thesis: verum
end;
end;