:: Affine Independence in Vector Spaces
:: by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

registration
let RLS be non empty RLSStruct ;
let A be empty Subset of RLS;
cluster conv A ->  empty ;
coherence
 conv A is empty
proofend;
end;

Lm1:  for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A
proofend;

registration
let RLS be non empty RLSStruct ;
let A be non empty Subset of RLS;
cluster conv A ->  non empty ;
coherence
 not conv A is empty
proofend;
end;

theorem :: RLAFFIN1:1
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v being Element of R holds conv {v} = {v}
proofend;

theorem :: RLAFFIN1:2
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A by Lm1;

theorem Th3: :: RLAFFIN1:3
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
conv A c= conv B
proofend;

theorem :: RLAFFIN1:4
for RLS being non empty RLSStruct
for S, A being Subset of RLS st A c= conv S holds
conv S = conv (S \/ A)
proofend;

Lm2:  for V being non empty right_complementable add-associative right_zeroed addLoopStr
for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
proofend;

Lm3:  for S being non empty addLoopStr
for v, w being Element of S holds {(v + w)} = v + {w}
proofend;

theorem Th5: :: RLAFFIN1:5
for V being non empty add-associative addLoopStr
for A being Subset of V
for v, w being Element of V holds (v + w) + A = v + (w + A)
proofend;

theorem Th6: :: RLAFFIN1:6
for V being non empty Abelian right_zeroed addLoopStr
for A being Subset of V holds (0. V) + A = A
proofend;

Lm4:  for V being non empty addLoopStr
for A being Subset of V
for v being Element of V holds card (v + A) c= card A
proofend;

theorem Th7: :: RLAFFIN1:7
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for g being Element of G
for A being Subset of G holds card A = card (g + A)
proofend;

theorem Th8: :: RLAFFIN1:8
for S being non empty addLoopStr
for v being Element of S holds v + ({} S) = {} S
proofend;

theorem Th9: :: RLAFFIN1:9
for r being Real
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
r * A c= r * B
proofend;

theorem Th10: :: RLAFFIN1:10
for r, s being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R holds (r * s) * AR = r * (s * AR)
proofend;

theorem Th11: :: RLAFFIN1:11
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R holds 1 * AR = AR
proofend;

theorem Th12: :: RLAFFIN1:12
for V being RealLinearSpace
for A being Subset of V holds 0 * A c= {(0. V)}
proofend;

theorem Th13: :: RLAFFIN1:13
for S being non empty addLoopStr
for LS1, LS2 being Linear_Combination of S
for F being FinSequence of S holds (LS1 + LS2) * F = (LS1 * F) + (LS2 * F)
proofend;

theorem Th14: :: RLAFFIN1:14
for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V
for F being FinSequence of V holds (r * L) * F = r * (L * F)
proofend;

theorem Th15: :: RLAFFIN1:15
for V being RealLinearSpace
for A, B being Subset of V st A is linearly-independent & A c= B & Lin B = V holds
ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V )
proofend;

begin

definition
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let LG be Linear_Combination of G;
let g be Element of G;
funcg + LG ->  Linear_Combination of G means :Def1: :: RLAFFIN1:def 1
 for h being Element of G holds it . h = LG . (h - g);
existence
 ex b1 being Linear_Combination of G st
for h being Element of G holds b1 . h = LG . (h - g)
proofend;
uniqueness
 for b1, b2 being Linear_Combination of G st ( for h being Element of G holds b1 . h = LG . (h - g) ) & ( for h being Element of G holds b2 . h = LG . (h - g) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines + RLAFFIN1:def_1_:_
 for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G
for b4 being Linear_Combination of G holds
( b4 = g + LG iff for h being Element of G holds b4 . h = LG . (h - g) );

theorem Th16: :: RLAFFIN1:16
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G holds Carrier (g + LG) = g + (Carrier LG)
proofend;

theorem Th17: :: RLAFFIN1:17
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG1, LG2 being Linear_Combination of G
for g being Element of G holds g + (LG1 + LG2) = (g + LG1) + (g + LG2)
proofend;

theorem :: RLAFFIN1:18
for r being Real
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
proofend;

theorem Th19: :: RLAFFIN1:19
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g, h being Element of G holds g + (h + LG) = (g + h) + LG
proofend;

theorem Th20: :: RLAFFIN1:20
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for g being Element of G holds g + (ZeroLC G) = ZeroLC G
proofend;

theorem Th21: :: RLAFFIN1:21
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G holds (0. G) + LG = LG
proofend;

definition
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
let LR be Linear_Combination of R;
let r be Real;
funcr (*) LR ->  Linear_Combination of R means :Def2: :: RLAFFIN1:def 2
 for v being Element of R holds it . v = LR . ((r ") * v) if r <> 0
otherwise it = ZeroLC R;
existence
 ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) &amp; ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) )
proofend;
uniqueness
 for b1, b2 being Linear_Combination of R holds
( ( r <> 0 &amp; ( for v being Element of R holds b1 . v = LR . ((r ") * v) ) &amp; ( for v being Element of R holds b2 . v = LR . ((r ") * v) ) implies b1 = b2 ) &amp; ( not r <> 0 &amp; b1 = ZeroLC R &amp; b2 = ZeroLC R implies b1 = b2 ) )
proofend;
consistency
 for b1 being Linear_Combination of R holds verum ;
end;

:: deftheorem Def2 defines (*) RLAFFIN1:def_2_:_
 for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R
for r being Real
for b4 being Linear_Combination of R holds
( ( r <> 0 implies ( b4 = r (*) LR iff for v being Element of R holds b4 . v = LR . ((r ") * v) ) ) &amp; ( not r <> 0 implies ( b4 = r (*) LR iff b4 = ZeroLC R ) ) );

theorem Th22: :: RLAFFIN1:22
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds Carrier (r (*) LR) c= r * (Carrier LR)
proofend;

theorem Th23: :: RLAFFIN1:23
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R st r <> 0 holds
Carrier (r (*) LR) = r * (Carrier LR)
proofend;

theorem Th24: :: RLAFFIN1:24
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
proofend;

theorem :: RLAFFIN1:25
for r, s being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)
proofend;

theorem Th26: :: RLAFFIN1:26
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds r (*) (ZeroLC R) = ZeroLC R
proofend;

theorem Th27: :: RLAFFIN1:27
for r, s being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds r (*) (s (*) LR) = (r * s) (*) LR
proofend;

theorem Th28: :: RLAFFIN1:28
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds 1 (*) LR = LR
proofend;

begin

definition
let S be non empty addLoopStr ;
let LS be Linear_Combination of S;
func sum LS ->  Real means :Def3: :: RLAFFIN1:def 3
 ex F being FinSequence of S st
( F is one-to-one &amp; rng F = Carrier LS &amp; it = Sum (LS * F) );
existence
 ex b1 being Real ex F being FinSequence of S st
( F is one-to-one &amp; rng F = Carrier LS &amp; b1 = Sum (LS * F) )
proofend;
uniqueness
 for b1, b2 being Real st ex F being FinSequence of S st
( F is one-to-one &amp; rng F = Carrier LS &amp; b1 = Sum (LS * F) ) &amp; ex F being FinSequence of S st
( F is one-to-one &amp; rng F = Carrier LS &amp; b2 = Sum (LS * F) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines sum RLAFFIN1:def_3_:_
 for S being non empty addLoopStr
for LS being Linear_Combination of S
for b3 being Real holds
( b3 = sum LS iff ex F being FinSequence of S st
( F is one-to-one &amp; rng F = Carrier LS &amp; b3 = Sum (LS * F) ) );

theorem Th29: :: RLAFFIN1:29
for S being non empty addLoopStr
for LS being Linear_Combination of S
for F being FinSequence of S st Carrier LS misses rng F holds
Sum (LS * F) = 0
proofend;

theorem Th30: :: RLAFFIN1:30
for S being non empty addLoopStr
for LS being Linear_Combination of S
for F being FinSequence of S st F is one-to-one &amp; Carrier LS c= rng F holds
sum LS = Sum (LS * F)
proofend;

theorem Th31: :: RLAFFIN1:31
for S being non empty addLoopStr holds sum (ZeroLC S) = 0
proofend;

theorem Th32: :: RLAFFIN1:32
for S being non empty addLoopStr
for LS being Linear_Combination of S
for v being Element of S st Carrier LS c= {v} holds
sum LS = LS . v
proofend;

theorem :: RLAFFIN1:33
for S being non empty addLoopStr
for LS being Linear_Combination of S
for v1, v2 being Element of S st Carrier LS c= {v1,v2} &amp; v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
proofend;

theorem Th34: :: RLAFFIN1:34
for S being non empty addLoopStr
for LS1, LS2 being Linear_Combination of S holds sum (LS1 + LS2) = (sum LS1) + (sum LS2)
proofend;

theorem Th35: :: RLAFFIN1:35
for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds sum (r * L) = r * (sum L)
proofend;

theorem Th36: :: RLAFFIN1:36
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds sum (L1 - L2) = (sum L1) - (sum L2)
proofend;

theorem Th37: :: RLAFFIN1:37
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G holds sum LG = sum (g + LG)
proofend;

theorem Th38: :: RLAFFIN1:38
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R st r <> 0 holds
sum LR = sum (r (*) LR)
proofend;

theorem Th39: :: RLAFFIN1:39
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)
proofend;

theorem Th40: :: RLAFFIN1:40
for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)
proofend;

begin

definition
let V be RealLinearSpace;
let A be Subset of V;
attrA is affinely-independent  means :Def4: :: RLAFFIN1:def 4
( A is empty or ex v being VECTOR of V st
( v in A &amp; ((- v) + A) \ {(0. V)} is linearly-independent ) );
end;

:: deftheorem Def4 defines affinely-independent RLAFFIN1:def_4_:_
 for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff ( A is empty or ex v being VECTOR of V st
( v in A &amp; ((- v) + A) \ {(0. V)} is linearly-independent ) ) );

registration
let V be RealLinearSpace;
cluster empty  ->  affinely-independent for Element of K19( the carrier of V);
coherence
 for b1 being Subset of V st b1 is empty holds
b1 is affinely-independent by Def4;
let v be VECTOR of V;
cluster{v} ->  affinely-independent for Subset of V;
coherence
 for b1 being Subset of V st b1 = {v} holds
b1 is affinely-independent
proofend;
let w be VECTOR of V;
cluster{v,w} ->  affinely-independent for Subset of V;
coherence
 for b1 being Subset of V st b1 = {v,w} holds
b1 is affinely-independent
proofend;
end;

registration
let V be RealLinearSpace;
cluster1 -element affinely-independent for Element of K19( the carrier of V);
existence
 ex b1 being Subset of V st
( b1 is 1 -element &amp; b1 is affinely-independent )
proofend;
end;

Lm5:  for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V &amp; sum L = 0 holds
Carrier L = {}
proofend;

Lm6:  for V being RealLinearSpace
for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V &amp; sum L = 0 holds
Carrier L = {} ) holds
for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
proofend;

theorem Th41: :: RLAFFIN1:41
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent )
proofend;

theorem Th42: :: RLAFFIN1:42
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V &amp; sum L = 0 holds
Carrier L = {} )
proofend;

theorem Th43: :: RLAFFIN1:43
for V being RealLinearSpace
for A, B being Subset of V st A is affinely-independent &amp; B c= A holds
B is affinely-independent
proofend;

registration
let V be RealLinearSpace;
cluster linearly-independent  ->  affinely-independent for Element of K19( the carrier of V);
coherence
 for b1 being Subset of V st b1 is linearly-independent holds
b1 is affinely-independent
proofend;
end;

registration
let V be RealLinearSpace;
let I be affinely-independent Subset of V;
let v be VECTOR of V;
clusterv + I ->  affinely-independent ;
coherence
 v + I is affinely-independent
proofend;
end;

theorem :: RLAFFIN1:44
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v + A is affinely-independent holds
A is affinely-independent
proofend;

registration
let V be RealLinearSpace;
let I be affinely-independent Subset of V;
let r be Real;
clusterr * I ->  affinely-independent ;
coherence
 r * I is affinely-independent
proofend;
end;

theorem :: RLAFFIN1:45
for r being Real
for V being RealLinearSpace
for A being Subset of V st r * A is affinely-independent &amp; r <> 0 holds
A is affinely-independent
proofend;

theorem Th46: :: RLAFFIN1:46
for V being RealLinearSpace
for A being Subset of V st 0. V in A holds
( A is affinely-independent iff A \ {(0. V)} is linearly-independent )
proofend;

definition
let V be RealLinearSpace;
let F be Subset-Family of V;
attrF is affinely-independent  means :Def5: :: RLAFFIN1:def 5
 for A being Subset of V st A in F holds
A is affinely-independent ;
end;

:: deftheorem Def5 defines affinely-independent RLAFFIN1:def_5_:_
 for V being RealLinearSpace
for F being Subset-Family of V holds
( F is affinely-independent iff for A being Subset of V st A in F holds
A is affinely-independent );

registration
let V be RealLinearSpace;
cluster empty  ->  affinely-independent for Element of K19(K19( the carrier of V));
coherence
 for b1 being Subset-Family of V st b1 is empty holds
b1 is affinely-independent
proofend;
let I be affinely-independent Subset of V;
cluster{I} ->  affinely-independent for Subset-Family of V;
coherence
 for b1 being Subset-Family of V st b1 = {I} holds
b1 is affinely-independent
proofend;
end;

registration
let V be RealLinearSpace;
cluster empty affinely-independent for Element of K19(K19( the carrier of V));
existence
 ex b1 being Subset-Family of V st
( b1 is empty &amp; b1 is affinely-independent )
proofend;
cluster non empty affinely-independent for Element of K19(K19( the carrier of V));
existence
 ex b1 being Subset-Family of V st
( not b1 is empty &amp; b1 is affinely-independent )
proofend;
end;

theorem :: RLAFFIN1:47
for V being RealLinearSpace
for F1, F2 being Subset-Family of V st F1 is affinely-independent &amp; F2 is affinely-independent holds
F1 \/ F2 is affinely-independent
proofend;

theorem :: RLAFFIN1:48
for V being RealLinearSpace
for F1, F2 being Subset-Family of V st F1 c= F2 &amp; F2 is affinely-independent holds
F1 is affinely-independent
proofend;

begin

definition
let RLS be non empty RLSStruct ;
let A be Subset of RLS;
func Affin A ->  Subset of RLS equals :: RLAFFIN1:def 6
 meet  {  B where B is Affine Subset of RLS : A c= B  }  ;
coherence
 meet  {  B where B is Affine Subset of RLS : A c= B  }  is Subset of RLS
proofend;
end;

:: deftheorem  defines Affin RLAFFIN1:def_6_:_
 for RLS being non empty RLSStruct
for A being Subset of RLS holds Affin A = meet  {  B where B is Affine Subset of RLS : A c= B  }  ;

registration
let RLS be non empty RLSStruct ;
let A be Subset of RLS;
cluster Affin A ->  Affine ;
coherence
 Affin A is Affine
proofend;
end;

Lm7:  for V being non empty RLSStruct
for A being Subset of V holds A c= Affin A
proofend;

Lm8:  for V being non empty RLSStruct
for A being Affine Subset of V holds A = Affin A
proofend;

registration
let RLS be non empty RLSStruct ;
let A be empty Subset of RLS;
cluster Affin A ->  empty ;
coherence
 Affin A is empty
proofend;
end;

registration
let RLS be non empty RLSStruct ;
let A be non empty Subset of RLS;
cluster Affin A ->  non empty ;
coherence
 not Affin A is empty
proofend;
end;

theorem :: RLAFFIN1:49
for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= Affin A by Lm7;

theorem :: RLAFFIN1:50
for RLS being non empty RLSStruct
for A being Affine Subset of RLS holds A = Affin A by Lm8;

theorem Th51: :: RLAFFIN1:51
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B &amp; B is Affine holds
Affin A c= B
proofend;

theorem Th52: :: RLAFFIN1:52
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
Affin A c= Affin B
proofend;

theorem Th53: :: RLAFFIN1:53
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V holds Affin (v + A) = v + (Affin A)
proofend;

theorem Th54: :: RLAFFIN1:54
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R st AR is Affine holds
r * AR is Affine
proofend;

theorem Th55: :: RLAFFIN1:55
for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R st r <> 0 holds
Affin (r * AR) = r * (Affin AR)
proofend;

theorem :: RLAFFIN1:56
for r being Real
for V being RealLinearSpace
for A being Subset of V holds Affin (r * A) = r * (Affin A)
proofend;

theorem Th57: :: RLAFFIN1:57
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v in Affin A holds
Affin A = v + (Up (Lin ((- v) + A)))
proofend;

Lm9:  for V being RealLinearSpace
for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
proofend;

theorem Th58: :: RLAFFIN1:58
for V being RealLinearSpace
for A being Subset of V holds
( A is affinely-independent iff for B being Subset of V st B c= A &amp; Affin A = Affin B holds
A = B )
proofend;

theorem Th59: :: RLAFFIN1:59
for V being RealLinearSpace
for A being Subset of V holds Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }
proofend;

theorem Th60: :: RLAFFIN1:60
for V being RealLinearSpace
for A being Subset of V
for I being affinely-independent Subset of V st I c= A holds
ex Ia being affinely-independent Subset of V st
( I c= Ia &amp; Ia c= A &amp; Affin Ia = Affin A )
proofend;

theorem :: RLAFFIN1:61
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent &amp; Affin A = Affin B &amp; card B <= card A holds
B is affinely-independent
proofend;

theorem Th62: :: RLAFFIN1:62
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff ( sum L = 1 &amp; ( for v being VECTOR of V holds 0 <= L . v ) ) )
proofend;

theorem Th63: :: RLAFFIN1:63
for x being set
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
L . x <= 1
proofend;

theorem Th64: :: RLAFFIN1:64
for x being set
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex &amp; L . x = 1 holds
Carrier L = {x}
proofend;

theorem Th65: :: RLAFFIN1:65
for V being RealLinearSpace
for A being Subset of V holds conv A c= Affin A
proofend;

theorem :: RLAFFIN1:66
for x being set
for V being RealLinearSpace
for A being Subset of V st x in conv A &amp; (conv A) \ {x} is convex holds
x in A
proofend;

theorem Th67: :: RLAFFIN1:67
for V being RealLinearSpace
for A being Subset of V holds Affin (conv A) = Affin A
proofend;

theorem :: RLAFFIN1:68
for V being RealLinearSpace
for A, B being Subset of V st conv A c= conv B holds
Affin A c= Affin B
proofend;

theorem Th69: :: RLAFFIN1:69
for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= Affin B holds
Affin (A \/ B) = Affin B
proofend;

begin

definition
let V be RealLinearSpace;
let A be Subset of V;
assume B1: A is affinely-independent ;
let x be set ;
assume B2: x in Affin A ;
funcx |-- A ->  Linear_Combination of A means :Def7: :: RLAFFIN1:def 7
( Sum it = x &amp; sum it = 1 );
existence
 ex b1 being Linear_Combination of A st
( Sum b1 = x &amp; sum b1 = 1 )
proofend;
uniqueness
 for b1, b2 being Linear_Combination of A st Sum b1 = x &amp; sum b1 = 1 &amp; Sum b2 = x &amp; sum b2 = 1 holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines |-- RLAFFIN1:def_7_:_
 for V being RealLinearSpace
for A being Subset of V st A is affinely-independent holds
for x being set st x in Affin A holds
for b4 being Linear_Combination of A holds
( b4 = x |-- A iff ( Sum b4 = x &amp; sum b4 = 1 ) );

theorem Th70: :: RLAFFIN1:70
for r being Real
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for I being affinely-independent Subset of V st v1 in Affin I &amp; v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
proofend;

theorem Th71: :: RLAFFIN1:71
for x being set
for V being RealLinearSpace
for v being VECTOR of V
for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex &amp; 0 <= (x |-- I) . v &amp; (x |-- I) . v <= 1 )
proofend;

theorem Th72: :: RLAFFIN1:72
for x, y being set
for V being RealLinearSpace
for I being affinely-independent Subset of V st x in conv I holds
( (x |-- I) . y = 1 iff ( x = y &amp; x in I ) )
proofend;

theorem Th73: :: RLAFFIN1:73
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V st x in Affin I &amp; ( for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ) holds
x in conv I
proofend;

theorem :: RLAFFIN1:74
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V st x in I holds
(conv I) \ {x} is convex
proofend;

theorem Th75: :: RLAFFIN1:75
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in Affin I &amp; ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) &amp; x |-- I = x |-- (I \ B) )
proofend;

theorem :: RLAFFIN1:76
for x being set
for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in conv I &amp; ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
proofend;

theorem Th77: :: RLAFFIN1:77
for x being set
for V being RealLinearSpace
for B being Subset of V
for I being affinely-independent Subset of V st B c= I &amp; x in Affin B holds
x |-- B = x |-- I
proofend;

theorem Th78: :: RLAFFIN1:78
for r, s being Real
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for A being Subset of V st v1 in Affin A &amp; v2 in Affin A &amp; r + s = 1 holds
(r * v1) + (s * v2) in Affin A
proofend;

theorem Th79: :: RLAFFIN1:79
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent &amp; Affin A c= Affin B holds
card A <= card B
proofend;

theorem :: RLAFFIN1:80
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent &amp; Affin A c= Affin B &amp; card A = card B holds
B is affinely-independent
proofend;

theorem :: RLAFFIN1:81
for r, s being Real
for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
proofend;

theorem :: RLAFFIN1:82
for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent &amp; ( v in A or not v in Affin A ) ) )
proofend;

theorem :: RLAFFIN1:83
for r, s being Real
for V being RealLinearSpace
for w, v1, v2 being VECTOR of V
for A being Subset of V st not w in Affin A &amp; v1 in A &amp; v2 in A &amp; r <> 1 &amp; (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s &amp; v1 = v2 )
proofend;

theorem :: RLAFFIN1:84
for r being Real
for V being RealLinearSpace
for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I &amp; w in Affin I &amp; p in Affin (I \ {v}) &amp; w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
proofend;