:: RLAFFIN1 semantic presentation

begin


registration
let RLS be non empty RLSStruct ;
let A be empty Subset of RLS;
cluster conv A ->  empty ;
coherence
 conv A is empty
proof
 A = the empty convex Subset of RLS ;
then  A in Convex-Family A by CONVEX1:def_4;
hence  conv A is empty by SETFAM_1:4; ::_thesis: verum
end;
end;

Lm1:  for RLS being non empty RLSStruct
for A being Subset of RLS holds A c= conv A
proof
let RLS be non empty RLSStruct ; ::_thesis: for A being Subset of RLS holds A c= conv A
let A be Subset of RLS; ::_thesis: A c= conv A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in conv A )
assume A1: x in A ; ::_thesis: x in conv A
A2: now__::_thesis:_for_y_being_set_st_y_in_Convex-Family_A_holds_
x_in_y
let y be set ; ::_thesis: ( y in Convex-Family A implies x in y )
assume  y in Convex-Family A ; ::_thesis: x in y
then  A c= y by CONVEX1:def_4;
hence  x in y by A1; ::_thesis: verum
end;
 [#] RLS is convex by CONVEX1:16, RUSUB_4:22;
then  [#] RLS in Convex-Family A by CONVEX1:def_4;
hence  x in conv A by A2, SETFAM_1:def_1; ::_thesis: verum
end;

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
proof
 A c= conv A by Lm1;
hence  not conv A is empty ; ::_thesis: verum
end;
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}
proof
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for v being Element of R holds conv {v} = {v}
let v be Element of R; ::_thesis: conv {v} = {v}
 {v} is convex
proof
let u1, u2 be VECTOR of R; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u1 in {v} or not u2 in {v} or (b1 * u1) + ((1 - b1) * u2) in {v} )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u1 in {v} or not u2 in {v} or (r * u1) + ((1 - r) * u2) in {v} )
assume that
 0 < r and
 r < 1 ; ::_thesis: ( not u1 in {v} or not u2 in {v} or (r * u1) + ((1 - r) * u2) in {v} )
assume that
A1: u1 in {v} and
A2: u2 in {v} ; ::_thesis: (r * u1) + ((1 - r) * u2) in {v}
 ( u1 = v & u2 = v ) by A1, A2, TARSKI:def_1;
then (r * u1) + ((1 - r) * u2) = (r + (1 - r)) * u1 by RLVECT_1:def_6
.= u1 by RLVECT_1:def_8 ;
hence  (r * u1) + ((1 - r) * u2) in {v} by A1; ::_thesis: verum
end;
then  conv {v} c= {v} by CONVEX1:30;
hence  conv {v} = {v} by ZFMISC_1:33; ::_thesis: verum
end;

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
proof
let RLS be non empty RLSStruct ; ::_thesis: for A, B being Subset of RLS st A c= B holds
conv A c= conv B
let A, B be Subset of RLS; ::_thesis: ( A c= B implies conv A c= conv B )
assume A1: A c= B ; ::_thesis: conv A c= conv B
A2: Convex-Family B c= Convex-Family A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Convex-Family B or x in Convex-Family A )
assume A3: x in Convex-Family B ; ::_thesis: x in Convex-Family A
then reconsider X = x as Subset of RLS ;
 B c= X by A3, CONVEX1:def_4;
then A4: A c= X by A1, XBOOLE_1:1;
 X is convex by A3, CONVEX1:def_4;
hence  x in Convex-Family A by A4, CONVEX1:def_4; ::_thesis: verum
end;
 [#] RLS is convex by CONVEX1:16, RUSUB_4:22;
then  [#] RLS in Convex-Family B by CONVEX1:def_4;
then A5: meet (Convex-Family A) c= meet (Convex-Family B) by A2, SETFAM_1:6;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in conv A or y in conv B )
assume  y in conv A ; ::_thesis: y in conv B
hence  y in conv B by A5; ::_thesis: verum
end;

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)
proof
let RLS be non empty RLSStruct ; ::_thesis: for S, A being Subset of RLS st A c= conv S holds
conv S = conv (S \/ A)
let S, A be Subset of RLS; ::_thesis: ( A c= conv S implies conv S = conv (S \/ A) )
assume A1: A c= conv S ; ::_thesis: conv S = conv (S \/ A)
thus  conv S c= conv (S \/ A) by Th3, XBOOLE_1:7; :: according to XBOOLE_0:def_10 ::_thesis: conv (S \/ A) c= conv S
 S c= conv S by Lm1;
then  S \/ A c= conv S by A1, XBOOLE_1:8;
hence  conv (S \/ A) c= conv S by CONVEX1:30; ::_thesis: verum
end;

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)
proof
let V be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
let A, B be Subset of V; ::_thesis: for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
let v be Element of V; ::_thesis: (v + A) \ (v + B) = v + (A \ B)
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: v + (A \ B) c= (v + A) \ (v + B)
let x be set ; ::_thesis: ( x in (v + A) \ (v + B) implies x in v + (A \ B) )
assume A1: x in (v + A) \ (v + B) ; ::_thesis: x in v + (A \ B)
then  x in v + A by XBOOLE_0:def_5;
then consider w being Element of V such that
A2: x = v + w and
A3: w in A ;
 not x in v + B by A1, XBOOLE_0:def_5;
then  not w in B by A2;
then  w in A \ B by A3, XBOOLE_0:def_5;
hence  x in v + (A \ B) by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + (A \ B) or x in (v + A) \ (v + B) )
assume  x in v + (A \ B) ; ::_thesis: x in (v + A) \ (v + B)
then consider w being Element of V such that
A4: x = v + w and
A5: w in A \ B ;
A6: not x in v + B
proof
assume  x in v + B ; ::_thesis: contradiction
then consider s being Element of V such that
A7: x = v + s and
A8: s in B ;
 s = w by A4, A7, RLVECT_1:8;
hence  contradiction by A5, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
 w in A by A5, XBOOLE_0:def_5;
then  x in v + A by A4;
hence  x in (v + A) \ (v + B) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;

Lm3:  for S being non empty addLoopStr
for v, w being Element of S holds {(v + w)} = v + {w}
proof
let S be non empty addLoopStr ; ::_thesis: for v, w being Element of S holds {(v + w)} = v + {w}
let p, q be Element of S; ::_thesis: {(p + q)} = p + {q}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: p + {q} c= {(p + q)}
let x be set ; ::_thesis: ( x in {(p + q)} implies x in p + {q} )
assume  x in {(p + q)} ; ::_thesis: x in p + {q}
then A1: x = p + q by TARSKI:def_1;
 q in {q} by TARSKI:def_1;
hence  x in p + {q} by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in p + {q} or x in {(p + q)} )
assume  x in p + {q} ; ::_thesis: x in {(p + q)}
then consider v being Element of S such that
A2: x = p + v and
A3: v in {q} ;
 v = q by A3, TARSKI:def_1;
hence  x in {(p + q)} by A2, TARSKI:def_1; ::_thesis: verum
end;

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)
proof
let V be non empty add-associative addLoopStr ; ::_thesis: for A being Subset of V
for v, w being Element of V holds (v + w) + A = v + (w + A)
let A be Subset of V; ::_thesis: for v, w being Element of V holds (v + w) + A = v + (w + A)
let v, w be Element of V; ::_thesis: (v + w) + A = v + (w + A)
set vw = v + w;
thus  (v + w) + A c= v + (w + A) :: according to XBOOLE_0:def_10 ::_thesis: v + (w + A) c= (v + w) + A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (v + w) + A or x in v + (w + A) )
assume  x in (v + w) + A ; ::_thesis: x in v + (w + A)
then consider s being Element of V such that
A1: ( x = (v + w) + s & s in A ) ;
 ( w + s in w + A & x = v + (w + s) ) by A1, RLVECT_1:def_3;
hence  x in v + (w + A) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + (w + A) or x in (v + w) + A )
assume  x in v + (w + A) ; ::_thesis: x in (v + w) + A
then consider s being Element of V such that
A2: x = v + s and
A3: s in w + A ;
consider r being Element of V such that
A4: s = w + r and
A5: r in A by A3;
 x = (v + w) + r by A2, A4, RLVECT_1:def_3;
hence  x in (v + w) + A by A5; ::_thesis: verum
end;

theorem Th6: :: RLAFFIN1:6
for V being non empty Abelian right_zeroed addLoopStr
for A being Subset of V holds (0. V) + A = A
proof
let V be non empty Abelian right_zeroed addLoopStr ; ::_thesis: for A being Subset of V holds (0. V) + A = A
let A be Subset of V; ::_thesis: (0. V) + A = A
thus  (0. V) + A c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= (0. V) + A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (0. V) + A or x in A )
assume  x in (0. V) + A ; ::_thesis: x in A
then  ex s being Element of V st
( x = (0. V) + s & s in A ) ;
hence  x in A by RLVECT_1:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (0. V) + A )
assume A1: x in A ; ::_thesis: x in (0. V) + A
then reconsider v = x as Element of V ;
 (0. V) + v = v by RLVECT_1:def_4;
hence  x in (0. V) + A by A1; ::_thesis: verum
end;

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
proof
let V be non empty addLoopStr ; ::_thesis: for A being Subset of V
for v being Element of V holds card (v + A) c= card A
let A be Subset of V; ::_thesis: for v being Element of V holds card (v + A) c= card A
let v be Element of V; ::_thesis: card (v + A) c= card A
deffunc H1( Element of V) ->  Element of the carrier of V = v + $1;
 card  {  H1(w) where w is Element of V : w in A  }  c= card A from TREES_2:sch_2();
hence  card (v + A) c= card A ; ::_thesis: verum
end;

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)
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for g being Element of G
for A being Subset of G holds card A = card (g + A)
let g be Element of G; ::_thesis: for A being Subset of G holds card A = card (g + A)
let A be Subset of G; ::_thesis: card A = card (g + A)
(- g) + (g + A) = ((- g) + g) + A by Th5
.= (0. G) + A by RLVECT_1:5
.= A by Th6 ;
then A1: card A c= card (g + A) by Lm4;
 card (g + A) c= card A by Lm4;
hence  card A = card (g + A) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th8: :: RLAFFIN1:8
for S being non empty addLoopStr
for v being Element of S holds v + ({} S) = {} S
proof
let S be non empty addLoopStr ; ::_thesis: for v being Element of S holds v + ({} S) = {} S
let v be Element of S; ::_thesis: v + ({} S) = {} S
assume  v + ({} S) <> {} S ; ::_thesis: contradiction
then consider x being set  such that
A1: x in v + ({} S) by XBOOLE_0:def_1;
 ex w being Element of S st
( x = v + w & w in {} S ) by A1;
hence  contradiction ; ::_thesis: verum
end;

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
proof
let r be Real; ::_thesis: for RLS being non empty RLSStruct
for A, B being Subset of RLS st A c= B holds
r * A c= r * B
let RLS be non empty RLSStruct ; ::_thesis: for A, B being Subset of RLS st A c= B holds
r * A c= r * B
let A, B be Subset of RLS; ::_thesis: ( A c= B implies r * A c= r * B )
assume A1: A c= B ; ::_thesis: r * A c= r * B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * A or x in r * B )
assume  x in r * A ; ::_thesis: x in r * B
then  ex v being Element of RLS st
( x = r * v & v in A ) ;
hence  x in r * B by A1; ::_thesis: verum
end;

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)
proof
let r, s be Real; ::_thesis: 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)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for AR being Subset of R holds (r * s) * AR = r * (s * AR)
let AR be Subset of R; ::_thesis: (r * s) * AR = r * (s * AR)
set rs = r * s;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: r * (s * AR) c= (r * s) * AR
let x be set ; ::_thesis: ( x in (r * s) * AR implies x in r * (s * AR) )
assume  x in (r * s) * AR ; ::_thesis: x in r * (s * AR)
then consider v being Element of R such that
A1: ( x = (r * s) * v & v in AR ) ;
 ( s * v in s * AR & x = r * (s * v) ) by A1, RLVECT_1:def_7;
hence  x in r * (s * AR) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (s * AR) or x in (r * s) * AR )
assume  x in r * (s * AR) ; ::_thesis: x in (r * s) * AR
then consider v being Element of R such that
A2: x = r * v and
A3: v in s * AR ;
consider w being Element of R such that
A4: v = s * w and
A5: w in AR by A3;
 (r * s) * w = x by A2, A4, RLVECT_1:def_7;
hence  x in (r * s) * AR by A5; ::_thesis: verum
end;

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
proof
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for AR being Subset of R holds 1 * AR = AR
let AR be Subset of R; ::_thesis: 1 * AR = AR
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: AR c= 1 * AR
let x be set ; ::_thesis: ( x in 1 * AR implies x in AR )
assume  x in 1 * AR ; ::_thesis: x in AR
then  ex v being Element of R st
( x = 1 * v & v in AR ) ;
hence  x in AR by RLVECT_1:def_8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AR or x in 1 * AR )
assume A1: x in AR ; ::_thesis: x in 1 * AR
reconsider v = x as Element of R by A1;
 x = 1 * v by RLVECT_1:def_8;
hence  x in 1 * AR by A1; ::_thesis: verum
end;

theorem Th12: :: RLAFFIN1:12
for V being RealLinearSpace
for A being Subset of V holds 0 * A c= {(0. V)}
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds 0 * A c= {(0. V)}
let A be Subset of V; ::_thesis: 0 * A c= {(0. V)}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in 0 * A or x in {(0. V)} )
assume  x in 0 * A ; ::_thesis: x in {(0. V)}
then  ex v being Element of V st
( x = 0 * v & v in A ) ;
then  x = 0. V by RLVECT_1:10;
hence  x in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;

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)
proof
let S be non empty addLoopStr ; ::_thesis: for LS1, LS2 being Linear_Combination of S
for F being FinSequence of S holds (LS1 + LS2) * F = (LS1 * F) + (LS2 * F)
let LS1, LS2 be Linear_Combination of S; ::_thesis: for F being FinSequence of S holds (LS1 + LS2) * F = (LS1 * F) + (LS2 * F)
let p be FinSequence of S; ::_thesis: (LS1 + LS2) * p = (LS1 * p) + (LS2 * p)
A1: len (LS1 * p) = len p by FINSEQ_2:33;
A2: len (LS2 * p) = len p by FINSEQ_2:33;
then reconsider L1p = LS1 * p, L2p = LS2 * p as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;
A3: len ((LS1 + LS2) * p) = len p by FINSEQ_2:33;
A4: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_p_holds_
((LS1_+_LS2)_*_p)_._k_=_(L1p_+_L2p)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len p implies ((LS1 + LS2) * p) . k = (L1p + L2p) . k )
assume A5: ( 1 <= k & k <= len p ) ; ::_thesis: ((LS1 + LS2) * p) . k = (L1p + L2p) . k
then  k in dom ((LS1 + LS2) * p) by A3, FINSEQ_3:25;
then A6: ((LS1 + LS2) * p) . k = (LS1 + LS2) . (p . k) by FUNCT_1:12;
 k in dom L1p by A1, A5, FINSEQ_3:25;
then A7: ( p . k in dom LS1 & L1p . k = LS1 . (p . k) ) by FUNCT_1:11, FUNCT_1:12;
 k in dom L2p by A2, A5, FINSEQ_3:25;
then A8: L2p . k = LS2 . (p . k) by FUNCT_1:12;
 dom LS1 = the carrier of S by FUNCT_2:def_1;
hence ((LS1 + LS2) * p) . k = (L1p . k) + (L2p . k) by A6, A8, A7, RLVECT_2:def_10
.= (L1p + L2p) . k by RVSUM_1:11 ;
::_thesis: verum
end;
 len (L1p + L2p) = len p by CARD_1:def_7;
hence  (LS1 + LS2) * p = (LS1 * p) + (LS2 * p) by A3, A4, FINSEQ_1:14; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V
for F being FinSequence of V holds (r * L) * F = r * (L * F)
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V
for F being FinSequence of V holds (r * L) * F = r * (L * F)
let L be Linear_Combination of V; ::_thesis: for F being FinSequence of V holds (r * L) * F = r * (L * F)
let p be FinSequence of V; ::_thesis: (r * L) * p = r * (L * p)
A1: len ((r * L) * p) = len p by FINSEQ_2:33;
A2: len (L * p) = len p by FINSEQ_2:33;
then reconsider rLp = (r * L) * p, Lp = L * p as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;
A3: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_p_holds_
rLp_._k_=_(r_*_Lp)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len p implies rLp . k = (r * Lp) . k )
assume A4: ( 1 <= k & k <= len p ) ; ::_thesis: rLp . k = (r * Lp) . k
then  k in dom Lp by A2, FINSEQ_3:25;
then A5: ( Lp . k = L . (p . k) & p . k in dom L ) by FUNCT_1:11, FUNCT_1:12;
 k in dom rLp by A1, A4, FINSEQ_3:25;
then A6: rLp . k = (r * L) . (p . k) by FUNCT_1:12;
 ( (r * Lp) . k = r * (Lp . k) & dom L = the carrier of V ) by FUNCT_2:def_1, RVSUM_1:44;
hence  rLp . k = (r * Lp) . k by A5, A6, RLVECT_2:def_11; ::_thesis: verum
end;
 len (r * Lp) = len p by CARD_1:def_7;
hence  (r * L) * p = r * (L * p) by A1, A3, FINSEQ_1:14; ::_thesis: verum
end;

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 )
proof
let V be RealLinearSpace; ::_thesis: 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 )
let A, B be Subset of V; ::_thesis: ( A is linearly-independent & A c= B & Lin B = V implies ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V ) )
assume that
A1: ( A is linearly-independent & A c= B ) and
A2: Lin B = V ; ::_thesis: ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V )
defpred S1[ set ] means  ex I being Subset of V st
( I = $1 & A c= I & I c= B & I is linearly-independent );
consider Q being set  such that
A3: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A4: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
A5: Z <> {} and
A6: Z c= Q and
A7: Z is c=-linear ; ::_thesis: union Z in Q
set W = union Z;
 union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume  x in union Z ; ::_thesis: x in the carrier of V
then consider X being set  such that
A8: x in X and
A9: X in Z by TARSKI:def_4;
 X in bool the carrier of V by A3, A6, A9;
hence  x in the carrier of V by A8; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
set y = the Element of Z;
 the Element of Z in Q by A5, A6, TARSKI:def_3;
then A10: ex I being Subset of V st
( I = the Element of Z & A c= I & I c= B & I is linearly-independent ) by A3;
A11: W is linearly-independent
proof
deffunc H1( set ) ->  set =  {  D where D is Subset of V : ( $1 in D & D in Z )  }  ;
let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A12: Sum l = 0. V and
A13: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A14: dom f = Carrier l and
A15: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A13, A14, RELAT_1:42;
A16: now__::_thesis:_not_{}_in_M
assume  {} in M ; ::_thesis: contradiction
then consider x being set  such that
A17: x in dom f and
A18: f . x = {} by FUNCT_1:def_3;
 Carrier l c= W by RLVECT_2:def_6;
then consider X being set  such that
A19: x in X and
A20: X in Z by A14, A17, TARSKI:def_4;
reconsider X = X as Subset of V by A3, A6, A20;
 X in  {  D where D is Subset of V : ( x in D & D in Z )  }  by A19, A20;
hence  contradiction by A14, A15, A17, A18; ::_thesis: verum
end;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
 the Element of M in M ;
then A21: union M <> {} by A16, ORDERS_1:6;
then A22: dom the Choice_Function of M = M by FUNCT_2:def_1;
A23: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume  X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set  such that
A24: x in dom the Choice_Function of M and
A25: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set  such that
A26: ( y in dom f & f . y = x ) by A22, A24, FUNCT_1:def_3;
A27: x =  {  D where D is Subset of V : ( y in D & D in Z )  }  by A14, A15, A26;
 X in x by A16, A22, A24, A25, ORDERS_1:def_1;
then  ex D being Subset of V st
( D = X & y in D & D in Z ) by A27;
hence  X in Z ; ::_thesis: verum
end;
A28: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume  ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then  ( X in Z & Y in Z ) by A23;
then  X,Y are_c=-comparable by A7, ORDINAL1:def_8;
hence  ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
 dom the Choice_Function of M is finite by A14, A22, FINSET_1:8;
then  rng the Choice_Function of M is finite by FINSET_1:8;
then  union (rng the Choice_Function of M) in rng the Choice_Function of M by A21, A28, CARD_2:62;
then  union (rng the Choice_Function of M) in Z by A23;
then consider I being Subset of V such that
A29: I = union (rng the Choice_Function of M) and
 A c= I and
 I c= B and
A30: I is linearly-independent by A3, A6;
 Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
assume A31: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A32: f . x =  {  D where D is Subset of V : ( x in D & D in Z )  }  by A15;
A33: f . x in M by A14, A31, FUNCT_1:def_3;
then  the Choice_Function of M . (f . x) in f . x by A16, ORDERS_1:def_1;
then A34: ex D being Subset of V st
( the Choice_Function of M . (f . x) = D & x in D & D in Z ) by A32;
 the Choice_Function of M . (f . x) in rng the Choice_Function of M by A22, A33, FUNCT_1:def_3;
hence  x in union (rng the Choice_Function of M) by A34, TARSKI:def_4; ::_thesis: verum
end;
then  l is Linear_Combination of I by A29, RLVECT_2:def_6;
hence  contradiction by A12, A13, A30, RLVECT_3:def_1; ::_thesis: verum
end;
A35: W c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in B )
assume  x in W ; ::_thesis: x in B
then consider X being set  such that
A36: x in X and
A37: X in Z by TARSKI:def_4;
 ex I being Subset of V st
( I = X & A c= I & I c= B & I is linearly-independent ) by A3, A6, A37;
hence  x in B by A36; ::_thesis: verum
end;
 the Element of Z c= W by A5, ZFMISC_1:74;
then  A c= W by A10, XBOOLE_1:1;
hence  union Z in Q by A3, A11, A35; ::_thesis: verum
end;
 Q <> {} by A1, A3;
then consider X being set  such that
A38: X in Q and
A39: for Z being set st Z in Q & Z <> X holds
not X c= Z by A4, ORDERS_1:67;
consider I being Subset of V such that
A40: I = X and
A41: A c= I and
A42: I c= B and
A43: I is linearly-independent by A3, A38;
reconsider I = I as linearly-independent Subset of V by A43;
take  I ; ::_thesis: ( A c= I & I c= B & Lin I = V )
thus  ( A c= I & I c= B ) by A41, A42; ::_thesis: Lin I = V
assume A44: Lin I <> V ; ::_thesis: contradiction
now__::_thesis:_ex_v_being_VECTOR_of_V_st_
(_v_in_B_&_not_v_in_Lin_I_)
assume A45: for v being VECTOR of V st v in B holds
v in Lin I ; ::_thesis: contradiction
now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_B_holds_
v_in_Lin_I
let v be VECTOR of V; ::_thesis: ( v in Lin B implies v in Lin I )
assume  v in Lin B ; ::_thesis: v in Lin I
then consider l being Linear_Combination of B such that
A46: v = Sum l by RLVECT_3:14;
 Carrier l c= the carrier of (Lin I)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in the carrier of (Lin I) )
assume A47: x in Carrier l ; ::_thesis: x in the carrier of (Lin I)
then reconsider a = x as VECTOR of V ;
 Carrier l c= B by RLVECT_2:def_6;
then  a in Lin I by A45, A47;
hence  x in the carrier of (Lin I) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider l = l as Linear_Combination of Up (Lin I) by RLVECT_2:def_6;
 Sum l = v by A46;
then  v in Lin (Up (Lin I)) by RLVECT_3:14;
hence  v in Lin I by RLVECT_3:18; ::_thesis: verum
end;
then  Lin B is Subspace of Lin I by RLSUB_1:29;
hence  contradiction by A2, A44, RLSUB_1:26; ::_thesis: verum
end;
then consider v being VECTOR of V such that
A48: v in B and
A49: not v in Lin I ;
A50: not v in I by A49, RLVECT_3:15;
 {v} c= B by A48, ZFMISC_1:31;
then A51: I \/ {v} c= B by A42, XBOOLE_1:8;
 v in {v} by TARSKI:def_1;
then A52: v in I \/ {v} by XBOOLE_0:def_3;
A53: I \/ {v} is linearly-independent
proof
let l be Linear_Combination of I \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A54: Sum l = 0. V ; ::_thesis: Carrier l = {}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then A55: - (l . v) <> 0 by RLVECT_2:19;
deffunc H1( VECTOR of V) ->  Element of NAT = 0 ;
deffunc H2( VECTOR of V) ->  Element of REAL = l . $1;
consider f being Function of the carrier of V,REAL such that
A56: f . v = 0 and
A57: for u being Element of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_Element_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0
let u be Element of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 )
assume  not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0
then  ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then  ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1;
hence  f . u = 0 by A56, A57; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3;
 Carrier f c= I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in I )
assume  x in Carrier f ; ::_thesis: x in I
then consider u being Element of V such that
A58: u = x and
A59: f . u <> 0 ;
 f . u = l . u by A56, A57, A59;
then  ( Carrier l c= I \/ {v} & u in Carrier l ) by A59, RLVECT_2:def_6;
then  ( u in I or u in {v} ) by XBOOLE_0:def_3;
hence  x in I by A56, A58, A59, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of I by RLVECT_2:def_6;
consider g being Function of the carrier of V,REAL such that
A60: g . v = - (l . v) and
A61: for u being Element of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now__::_thesis:_for_u_being_Element_of_V_st_not_u_in_{v}_holds_
g_._u_=_0
let u be Element of V; ::_thesis: ( not u in {v} implies g . u = 0 )
assume  not u in {v} ; ::_thesis: g . u = 0
then  u <> v by TARSKI:def_1;
hence  g . u = 0 by A61; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3;
 Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume  x in Carrier g ; ::_thesis: x in {v}
then  ex u being Element of V st
( x = u & g . u <> 0 ) ;
then  x = v by A61;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6;
A62: Sum g = (- (l . v)) * v by A60, RLVECT_2:32;
now__::_thesis:_for_u_being_Element_of_V_holds_(f_-_g)_._u_=_l_._u
let u be Element of V; ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA63: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= l . u by A56, A60, A63 ; ::_thesis: verum
end;
supposeA64: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54
.= (l . u) - (g . u) by A57, A64
.= (l . u) - 0 by A61, A64
.= l . u ; ::_thesis: verum
end;
end;
end;
hence  (f - g) . u = l . u ; ::_thesis: verum
end;
then  f - g = l by RLVECT_2:def_9;
then  0. V = (Sum f) - (Sum g) by A54, RLVECT_3:4;
then  Sum f = (0. V) + (Sum g) by RLSUB_2:61
.= (- (l . v)) * v by A62, RLVECT_1:4 ;
then A65: (- (l . v)) * v in Lin I by RLVECT_3:14;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7
.= 1 * v by A55, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
hence  Carrier l = {} by A49, A65, RLSUB_1:21; ::_thesis: verum
end;
supposeA66: not v in Carrier l ; ::_thesis: Carrier l = {}
 Carrier l c= I
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in I )
assume A67: x in Carrier l ; ::_thesis: x in I
 Carrier l c= I \/ {v} by RLVECT_2:def_6;
then  ( x in I or x in {v} ) by A67, XBOOLE_0:def_3;
hence  x in I by A66, A67, TARSKI:def_1; ::_thesis: verum
end;
then  l is Linear_Combination of I by RLVECT_2:def_6;
hence  Carrier l = {} by A54, RLVECT_3:def_1; ::_thesis: verum
end;
end;
end;
 A c= I \/ {v} by A41, XBOOLE_1:10;
then  I \/ {v} in Q by A3, A51, A53;
hence  contradiction by A39, A40, A50, A52, XBOOLE_1:7; ::_thesis: verum
end;

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)
proof
deffunc H1( Element of G) ->  Element of the carrier of G = g + $1;
set vC =  {  H1(h) where h is Element of G : h in Carrier LG  }  ;
A1:  {  H1(h) where h is Element of G : h in Carrier LG  }  c= the carrier of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  H1(h) where h is Element of G : h in Carrier LG  }  or x in the carrier of G )
assume  x in  {  H1(h) where h is Element of G : h in Carrier LG  }  ; ::_thesis: x in the carrier of G
then  ex h being Element of G st
( x = H1(h) & h in Carrier LG ) ;
hence  x in the carrier of G ; ::_thesis: verum
end;
A2: Carrier LG is finite ;
  {  H1(h) where h is Element of G : h in Carrier LG  }  is finite from FRAENKEL:sch_21(A2);
then reconsider vC =  {  H1(h) where h is Element of G : h in Carrier LG  }  as finite Subset of G by A1;
deffunc H2( Element of G) ->  Element of REAL = LG . ($1 - g);
consider f being Function of the carrier of G,REAL such that
A3: for h being Element of G holds f . h = H2(h) from FUNCT_2:sch_4();
reconsider f = f as Element of Funcs ( the carrier of G,REAL) by FUNCT_2:8;
now__::_thesis:_for_h_being_Element_of_G_st_not_h_in_vC_holds_
not_f_._h_<>_0
let h be Element of G; ::_thesis: ( not h in vC implies not f . h <> 0 )
assume A4: not h in vC ; ::_thesis: not f . h <> 0
assume  f . h <> 0 ; ::_thesis: contradiction
then  LG . (h - g) <> 0 by A3;
then A5: h - g in Carrier LG ;
g + (h - g) = (h + (- g)) + g by RLVECT_1:def_11
.= h + (g + (- g)) by RLVECT_1:def_3
.= h + (0. G) by RLVECT_1:def_10
.= h by RLVECT_1:4 ;
hence  contradiction by A4, A5; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of G by RLVECT_2:def_3;
take  f ; ::_thesis: for h being Element of G holds f . h = LG . (h - g)
thus  for h being Element of G holds f . h = LG . (h - g) by A3; ::_thesis: verum
end;
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
proof
let L1, L2 be Linear_Combination of G; ::_thesis: ( ( for h being Element of G holds L1 . h = LG . (h - g) ) & ( for h being Element of G holds L2 . h = LG . (h - g) ) implies L1 = L2 )
assume that
A6: for h being Element of G holds L1 . h = LG . (h - g) and
A7: for h being Element of G holds L2 . h = LG . (h - g) ; ::_thesis: L1 = L2
now__::_thesis:_for_h_being_Element_of_G_holds_L1_._h_=_L2_._h
let h be Element of G; ::_thesis: L1 . h = L2 . h
thus L1 . h = LG . (h - g) by A6
.= L2 . h by A7 ; ::_thesis: verum
end;
hence  L1 = L2 by RLVECT_2:def_9; ::_thesis: verum
end;
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)
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for LG being Linear_Combination of G
for g being Element of G holds Carrier (g + LG) = g + (Carrier LG)
let LG be Linear_Combination of G; ::_thesis: for g being Element of G holds Carrier (g + LG) = g + (Carrier LG)
let g be Element of G; ::_thesis: Carrier (g + LG) = g + (Carrier LG)
thus  Carrier (g + LG) c= g + (Carrier LG) :: according to XBOOLE_0:def_10 ::_thesis: g + (Carrier LG) c= Carrier (g + LG)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (g + LG) or x in g + (Carrier LG) )
assume A1: x in Carrier (g + LG) ; ::_thesis: x in g + (Carrier LG)
reconsider w = x as Element of G by A1;
A2: (g + LG) . w <> 0 by A1, RLVECT_2:19;
A3: g + (w - g) = (w + (- g)) + g by RLVECT_1:def_11
.= w + (g + (- g)) by RLVECT_1:def_3
.= w + (0. G) by RLVECT_1:def_10
.= w by RLVECT_1:4 ;
 (g + LG) . w = LG . (w - g) by Def1;
then  w - g in Carrier LG by A2;
hence  x in g + (Carrier LG) by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g + (Carrier LG) or x in Carrier (g + LG) )
assume  x in g + (Carrier LG) ; ::_thesis: x in Carrier (g + LG)
then consider w being Element of G such that
A4: x = g + w and
A5: w in Carrier LG ;
(g + w) - g = (g + w) + (- g) by RLVECT_1:def_11
.= ((- g) + g) + w by RLVECT_1:def_3
.= (0. G) + w by RLVECT_1:5
.= w by RLVECT_1:4 ;
then A6: (g + LG) . (g + w) = LG . w by Def1;
 LG . w <> 0 by A5, RLVECT_2:19;
hence  x in Carrier (g + LG) by A4, A6; ::_thesis: verum
end;

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)
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for LG1, LG2 being Linear_Combination of G
for g being Element of G holds g + (LG1 + LG2) = (g + LG1) + (g + LG2)
let LG1, LG2 be Linear_Combination of G; ::_thesis: for g being Element of G holds g + (LG1 + LG2) = (g + LG1) + (g + LG2)
let g be Element of G; ::_thesis: g + (LG1 + LG2) = (g + LG1) + (g + LG2)
now__::_thesis:_for_h_being_Element_of_G_holds_(g_+_(LG1_+_LG2))_._h_=_((g_+_LG1)_+_(g_+_LG2))_._h
let h be Element of G; ::_thesis: (g + (LG1 + LG2)) . h = ((g + LG1) + (g + LG2)) . h
thus (g + (LG1 + LG2)) . h = (LG1 + LG2) . (h - g) by Def1
.= (LG1 . (h - g)) + (LG2 . (h - g)) by RLVECT_2:def_10
.= ((g + LG1) . h) + (LG2 . (h - g)) by Def1
.= ((g + LG1) . h) + ((g + LG2) . h) by Def1
.= ((g + LG1) + (g + LG2)) . h by RLVECT_2:def_10 ; ::_thesis: verum
end;
hence  g + (LG1 + LG2) = (g + LG1) + (g + LG2) by RLVECT_2:def_9; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
let L be Linear_Combination of V; ::_thesis: v + (r * L) = r * (v + L)
now__::_thesis:_for_w_being_VECTOR_of_V_holds_(v_+_(r_*_L))_._w_=_(r_*_(v_+_L))_._w
let w be VECTOR of V; ::_thesis: (v + (r * L)) . w = (r * (v + L)) . w
thus (v + (r * L)) . w = (r * L) . (w - v) by Def1
.= r * (L . (w - v)) by RLVECT_2:def_11
.= r * ((v + L) . w) by Def1
.= (r * (v + L)) . w by RLVECT_2:def_11 ; ::_thesis: verum
end;
hence  v + (r * L) = r * (v + L) by RLVECT_2:def_9; ::_thesis: verum
end;

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
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for LG being Linear_Combination of G
for g, h being Element of G holds g + (h + LG) = (g + h) + LG
let LG be Linear_Combination of G; ::_thesis: for g, h being Element of G holds g + (h + LG) = (g + h) + LG
let g, h be Element of G; ::_thesis: g + (h + LG) = (g + h) + LG
now__::_thesis:_for_s_being_Element_of_G_holds_(g_+_(h_+_LG))_._s_=_((g_+_h)_+_LG)_._s
let s be Element of G; ::_thesis: (g + (h + LG)) . s = ((g + h) + LG) . s
thus (g + (h + LG)) . s = (h + LG) . (s - g) by Def1
.= LG . ((s - g) - h) by Def1
.= LG . (s - (g + h)) by RLVECT_1:27
.= ((g + h) + LG) . s by Def1 ; ::_thesis: verum
end;
hence  g + (h + LG) = (g + h) + LG by RLVECT_2:def_9; ::_thesis: verum
end;

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
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for g being Element of G holds g + (ZeroLC G) = ZeroLC G
let g be Element of G; ::_thesis: g + (ZeroLC G) = ZeroLC G
 Carrier (ZeroLC G) = {} G by RLVECT_2:def_5;
then  {} G = g + (Carrier (ZeroLC G)) by Th8
.= Carrier (g + (ZeroLC G)) by Th16 ;
hence  g + (ZeroLC G) = ZeroLC G by RLVECT_2:def_5; ::_thesis: verum
end;

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
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for LG being Linear_Combination of G holds (0. G) + LG = LG
let LG be Linear_Combination of G; ::_thesis: (0. G) + LG = LG
now__::_thesis:_for_g_being_Element_of_G_holds_((0._G)_+_LG)_._g_=_LG_._g
let g be Element of G; ::_thesis: ((0. G) + LG) . g = LG . g
thus ((0. G) + LG) . g = LG . (g - (0. G)) by Def1
.= LG . g by RLVECT_1:13 ; ::_thesis: verum
end;
hence  (0. G) + LG = LG by RLVECT_2:def_9; ::_thesis: verum
end;

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) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) )
proof
now__::_thesis:_(_r_<>_0_implies_ex_f_being_Linear_Combination_of_R_st_
for_v_being_Element_of_R_holds_
(_(_r_<>_0_implies_ex_b3_being_Linear_Combination_of_R_st_
for_v_being_Element_of_R_holds_b3_._v_=_LR_._((r_")_*_v)_)_&_(_not_r_<>_0_implies_ex_b3_being_Linear_Combination_of_R_st_b3_=_ZeroLC_R_)_)_)
deffunc H1( Element of R) ->  Element of REAL = LR . ((r ") * $1);
deffunc H2( Element of R) ->  Element of the carrier of R = r * $1;
consider f being Function of the carrier of R,REAL such that
A1: for v being Element of R holds f . v = H1(v) from FUNCT_2:sch_4();
reconsider f = f as Element of Funcs ( the carrier of R,REAL) by FUNCT_2:8;
assume A2: r <> 0 ; ::_thesis: ex f being Linear_Combination of R st
for v being Element of R holds
( ( r <> 0 implies ex b3 being Linear_Combination of R st
for v being Element of R holds b3 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b3 being Linear_Combination of R st b3 = ZeroLC R ) )
A3: now__::_thesis:_for_v_being_Element_of_R_st_not_v_in_r_*_(Carrier_LR)_holds_
not_f_._v_<>_0
let v be Element of R; ::_thesis: ( not v in r * (Carrier LR) implies not f . v <> 0 )
assume A4: not v in r * (Carrier LR) ; ::_thesis: not f . v <> 0
A5: f . v = LR . ((r ") * v) by A1;
A6: r * ((r ") * v) = (r * (r ")) * v by RLVECT_1:def_7
.= 1 * v by A2, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
assume  f . v <> 0 ; ::_thesis: contradiction
then  (r ") * v in Carrier LR by A5;
hence  contradiction by A4, A6; ::_thesis: verum
end;
A7: Carrier LR is finite ;
  {  H2(w) where w is Element of R : w in Carrier LR  }  is finite from FRAENKEL:sch_21(A7);
then reconsider f = f as Linear_Combination of R by A3, RLVECT_2:def_3;
take f = f; ::_thesis: for v being Element of R holds
( ( r <> 0 implies ex b2 being Linear_Combination of R st
for v being Element of R holds b2 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b2 being Linear_Combination of R st b2 = ZeroLC R ) )
let v be Element of R; ::_thesis: ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) )
 f . v = LR . ((r ") * v) by A1;
hence  ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) ) by A1; ::_thesis: verum
end;
hence  ( ( r <> 0 implies ex b1 being Linear_Combination of R st
for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( not r <> 0 implies ex b1 being Linear_Combination of R st b1 = ZeroLC R ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Linear_Combination of R holds
( ( r <> 0 & ( for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds b2 . v = LR . ((r ") * v) ) implies b1 = b2 ) & ( not r <> 0 & b1 = ZeroLC R & b2 = ZeroLC R implies b1 = b2 ) )
proof
now__::_thesis:_for_L1,_L2_being_Linear_Combination_of_R_st_(_for_v_being_Element_of_R_holds_L1_._v_=_LR_._((r_")_*_v)_)_&_(_for_v_being_Element_of_R_holds_L2_._v_=_LR_._((r_")_*_v)_)_holds_
L1_=_L2
let L1, L2 be Linear_Combination of R; ::_thesis: ( ( for v being Element of R holds L1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds L2 . v = LR . ((r ") * v) ) implies L1 = L2 )
assume that
A8: for v being Element of R holds L1 . v = LR . ((r ") * v) and
A9: for v being Element of R holds L2 . v = LR . ((r ") * v) ; ::_thesis: L1 = L2
now__::_thesis:_for_v_being_Element_of_R_holds_L1_._v_=_L2_._v
let v be Element of R; ::_thesis: L1 . v = L2 . v
thus L1 . v = LR . ((r ") * v) by A8
.= L2 . v by A9 ; ::_thesis: verum
end;
hence  L1 = L2 by RLVECT_2:def_9; ::_thesis: verum
end;
hence  for b1, b2 being Linear_Combination of R holds
( ( r <> 0 & ( for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds b2 . v = LR . ((r ") * v) ) implies b1 = b2 ) & ( not r <> 0 & b1 = ZeroLC R & b2 = ZeroLC R implies b1 = b2 ) ) ; ::_thesis: verum
end;
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) ) ) & ( 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)
proof
let r be Real; ::_thesis: 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)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for LR being Linear_Combination of R holds Carrier (r (*) LR) c= r * (Carrier LR)
let LR be Linear_Combination of R; ::_thesis: Carrier (r (*) LR) c= r * (Carrier LR)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (r (*) LR) or x in r * (Carrier LR) )
assume A1: x in Carrier (r (*) LR) ; ::_thesis: x in r * (Carrier LR)
reconsider v = x as Element of R by A1;
A2: (r (*) LR) . v <> 0 by A1, RLVECT_2:19;
 0 (*) LR = ZeroLC R by Def2;
then A3: r <> 0 by A1, RLVECT_2:def_5;
then  (r (*) LR) . v = LR . ((r ") * v) by Def2;
then A4: (r ") * v in Carrier LR by A2;
r * ((r ") * v) = (r * (r ")) * v by RLVECT_1:def_7
.= 1 * v by A3, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
hence  x in r * (Carrier LR) by A4; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: 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)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for LR being Linear_Combination of R st r <> 0 holds
Carrier (r (*) LR) = r * (Carrier LR)
let LR be Linear_Combination of R; ::_thesis: ( r <> 0 implies Carrier (r (*) LR) = r * (Carrier LR) )
assume A1: r <> 0 ; ::_thesis: Carrier (r (*) LR) = r * (Carrier LR)
thus  Carrier (r (*) LR) c= r * (Carrier LR) by Th22; :: according to XBOOLE_0:def_10 ::_thesis: r * (Carrier LR) c= Carrier (r (*) LR)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (Carrier LR) or x in Carrier (r (*) LR) )
assume  x in r * (Carrier LR) ; ::_thesis: x in Carrier (r (*) LR)
then consider v being Element of R such that
A2: x = r * v and
A3: v in Carrier LR ;
(r ") * (r * v) = ((r ") * r) * v by RLVECT_1:def_7
.= 1 * v by A1, XCMPLX_0:def_7
.= v by RLVECT_1:def_8 ;
then A4: LR . v = (r (*) LR) . x by A1, A2, Def2;
 LR . v <> 0 by A3, RLVECT_2:19;
hence  x in Carrier (r (*) LR) by A2, A4; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: 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)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for LR1, LR2 being Linear_Combination of R holds r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
let LR1, LR2 be Linear_Combination of R; ::_thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
percases ( r = 0 or r <> 0 ) ;
supposeA1: r = 0 ; ::_thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
set Z = ZeroLC R;
A2: now__::_thesis:_for_v_being_Element_of_R_holds_((ZeroLC_R)_+_(ZeroLC_R))_._v_=_(ZeroLC_R)_._v
let v be Element of R; ::_thesis: ((ZeroLC R) + (ZeroLC R)) . v = (ZeroLC R) . v
thus ((ZeroLC R) + (ZeroLC R)) . v = ((ZeroLC R) . v) + ((ZeroLC R) . v) by RLVECT_2:def_10
.= ((ZeroLC R) . v) + 0 by RLVECT_2:20
.= (ZeroLC R) . v ; ::_thesis: verum
end;
thus r (*) (LR1 + LR2) = ZeroLC R by A1, Def2
.= (ZeroLC R) + (ZeroLC R) by A2, RLVECT_2:def_9
.= (r (*) LR1) + (ZeroLC R) by A1, Def2
.= (r (*) LR1) + (r (*) LR2) by A1, Def2 ; ::_thesis: verum
end;
supposeA3: r <> 0 ; ::_thesis: r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2)
now__::_thesis:_for_v_being_Element_of_R_holds_(r_(*)_(LR1_+_LR2))_._v_=_((r_(*)_LR1)_+_(r_(*)_LR2))_._v
let v be Element of R; ::_thesis: (r (*) (LR1 + LR2)) . v = ((r (*) LR1) + (r (*) LR2)) . v
thus (r (*) (LR1 + LR2)) . v = (LR1 + LR2) . ((r ") * v) by A3, Def2
.= (LR1 . ((r ") * v)) + (LR2 . ((r ") * v)) by RLVECT_2:def_10
.= ((r (*) LR1) . v) + (LR2 . ((r ") * v)) by A3, Def2
.= ((r (*) LR1) . v) + ((r (*) LR2) . v) by A3, Def2
.= ((r (*) LR1) + (r (*) LR2)) . v by RLVECT_2:def_10 ; ::_thesis: verum
end;
hence  r (*) (LR1 + LR2) = (r (*) LR1) + (r (*) LR2) by RLVECT_2:def_9; ::_thesis: verum
end;
end;
end;

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)
proof
let r, s be Real; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds r * (s (*) L) = s (*) (r * L)
let L be Linear_Combination of V; ::_thesis: r * (s (*) L) = s (*) (r * L)
percases ( s = 0 or s <> 0 ) ;
supposeA1: s = 0 ; ::_thesis: r * (s (*) L) = s (*) (r * L)
hence r * (s (*) L) = r * (ZeroLC V) by Def2
.= r * (0 * L) by RLVECT_2:43
.= (r * 0) * L by RLVECT_2:47
.= ZeroLC V by RLVECT_2:43
.= s (*) (r * L) by A1, Def2 ;
::_thesis: verum
end;
supposeA2: s <> 0 ; ::_thesis: r * (s (*) L) = s (*) (r * L)
now__::_thesis:_for_v_being_VECTOR_of_V_holds_(r_*_(s_(*)_L))_._v_=_(s_(*)_(r_*_L))_._v
let v be VECTOR of V; ::_thesis: (r * (s (*) L)) . v = (s (*) (r * L)) . v
thus (r * (s (*) L)) . v = r * ((s (*) L) . v) by RLVECT_2:def_11
.= r * (L . ((s ") * v)) by A2, Def2
.= (r * L) . ((s ") * v) by RLVECT_2:def_11
.= (s (*) (r * L)) . v by A2, Def2 ; ::_thesis: verum
end;
hence  r * (s (*) L) = s (*) (r * L) by RLVECT_2:def_9; ::_thesis: verum
end;
end;
end;

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
proof
let r be Real; ::_thesis: for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds r (*) (ZeroLC R) = ZeroLC R
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: r (*) (ZeroLC R) = ZeroLC R
percases ( r = 0 or r <> 0 ) ;
suppose r = 0 ; ::_thesis: r (*) (ZeroLC R) = ZeroLC R
hence  r (*) (ZeroLC R) = ZeroLC R by Def2; ::_thesis: verum
end;
supposeA1: r <> 0 ; ::_thesis: r (*) (ZeroLC R) = ZeroLC R
now__::_thesis:_for_v_being_Element_of_R_holds_(r_(*)_(ZeroLC_R))_._v_=_(ZeroLC_R)_._v
let v be Element of R; ::_thesis: (r (*) (ZeroLC R)) . v = (ZeroLC R) . v
thus (r (*) (ZeroLC R)) . v = (ZeroLC R) . ((r ") * v) by A1, Def2
.= 0 by RLVECT_2:20
.= (ZeroLC R) . v by RLVECT_2:20 ; ::_thesis: verum
end;
hence  r (*) (ZeroLC R) = ZeroLC R by RLVECT_2:def_9; ::_thesis: verum
end;
end;
end;

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
proof
let r, s be Real; ::_thesis: 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
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for LR being Linear_Combination of R holds r (*) (s (*) LR) = (r * s) (*) LR
let LR be Linear_Combination of R; ::_thesis: r (*) (s (*) LR) = (r * s) (*) LR
percases ( r = 0 or s = 0 or ( r <> 0 & s <> 0 ) ) ;
supposeA1: ( r = 0 or s = 0 ) ; ::_thesis: r (*) (s (*) LR) = (r * s) (*) LR
then  (r * s) (*) LR = ZeroLC R by Def2;
hence  r (*) (s (*) LR) = (r * s) (*) LR by A1, Def2, Th26; ::_thesis: verum
end;
supposeA2: ( r <> 0 & s <> 0 ) ; ::_thesis: r (*) (s (*) LR) = (r * s) (*) LR
now__::_thesis:_for_v_being_Element_of_R_holds_(r_(*)_(s_(*)_LR))_._v_=_((r_*_s)_(*)_LR)_._v
let v be Element of R; ::_thesis: (r (*) (s (*) LR)) . v = ((r * s) (*) LR) . v
thus (r (*) (s (*) LR)) . v = (s (*) LR) . ((r ") * v) by A2, Def2
.= LR . ((s ") * ((r ") * v)) by A2, Def2
.= LR . (((s ") * (r ")) * v) by RLVECT_1:def_7
.= LR . (((r * s) ") * v) by XCMPLX_1:204
.= ((r * s) (*) LR) . v by A2, Def2 ; ::_thesis: verum
end;
hence  r (*) (s (*) LR) = (r * s) (*) LR by RLVECT_2:def_9; ::_thesis: verum
end;
end;
end;

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
proof
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for LR being Linear_Combination of R holds 1 (*) LR = LR
let LR be Linear_Combination of R; ::_thesis: 1 (*) LR = LR
now__::_thesis:_for_v_being_Element_of_R_holds_(1_(*)_LR)_._v_=_LR_._v
let v be Element of R; ::_thesis: (1 (*) LR) . v = LR . v
thus (1 (*) LR) . v = LR . ((1 ") * v) by Def2
.= LR . v by RLVECT_1:def_8 ; ::_thesis: verum
end;
hence  1 (*) LR = LR by RLVECT_2:def_9; ::_thesis: verum
end;

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 & rng F = Carrier LS & it = Sum (LS * F) );
existence
 ex b1 being Real ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b1 = Sum (LS * F) )
proof
consider p being FinSequence such that
A1: rng p = Carrier LS and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of S by A1, FINSEQ_1:def_4;
take  Sum (LS * p) ; ::_thesis: ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & Sum (LS * p) = Sum (LS * F) )
thus  ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & Sum (LS * p) = Sum (LS * F) ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b1 = Sum (LS * F) ) & ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & b2 = Sum (LS * F) ) holds
b1 = b2
proof
let S1, S2 be Real; ::_thesis: ( ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & S1 = Sum (LS * F) ) & ex F being FinSequence of S st
( F is one-to-one & rng F = Carrier LS & S2 = Sum (LS * F) ) implies S1 = S2 )
given F1 being FinSequence of S such that A3: F1 is one-to-one and
A4: rng F1 = Carrier LS and
A5: S1 = Sum (LS * F1) ; ::_thesis: ( for F being FinSequence of S holds
( not F is one-to-one or not rng F = Carrier LS or not S2 = Sum (LS * F) ) or S1 = S2 )
A6: dom (F1 ") = Carrier LS by A3, A4, FUNCT_1:33;
A7: len F1 = card (Carrier LS) by A3, A4, FINSEQ_4:62;
given F2 being FinSequence of S such that A8: F2 is one-to-one and
A9: rng F2 = Carrier LS and
A10: S2 = Sum (LS * F2) ; ::_thesis: S1 = S2
set F12 = (F1 ") * F2;
 ( dom F2 = Seg (len F2) & len F2 = card (Carrier LS) ) by A8, A9, FINSEQ_1:def_3, FINSEQ_4:62;
then A11: dom ((F1 ") * F2) = Seg (len F1) by A6, A7, A9, RELAT_1:27;
 dom F1 = Seg (len F1) by FINSEQ_1:def_3;
then  rng (F1 ") = Seg (len F1) by A3, FUNCT_1:33;
then A12: rng ((F1 ") * F2) = Seg (len F1) by A6, A9, RELAT_1:28;
then reconsider F12 = (F1 ") * F2 as Function of (Seg (len F1)),(Seg (len F1)) by A11, FUNCT_2:1;
A13: F12 is onto by A12, FUNCT_2:def_3;
 len (LS * F1) = len F1 by FINSEQ_2:33;
then  dom (LS * F1) = Seg (len F1) by FINSEQ_1:def_3;
then reconsider F12 = F12 as Permutation of (dom (LS * F1)) by A3, A8, A13;
(LS * F1) * F12 = LS * (F1 * F12) by RELAT_1:36
.= LS * ((F1 * (F1 ")) * F2) by RELAT_1:36
.= LS * ((id (Carrier LS)) * F2) by A3, A4, FUNCT_1:39
.= LS * F2 by A9, RELAT_1:53 ;
hence  S1 = S2 by A5, A10, FINSOP_1:7; ::_thesis: verum
end;
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 & rng F = Carrier LS & 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
proof
let S be non empty addLoopStr ; ::_thesis: for LS being Linear_Combination of S
for F being FinSequence of S st Carrier LS misses rng F holds
Sum (LS * F) = 0
let LS be Linear_Combination of S; ::_thesis: for F being FinSequence of S st Carrier LS misses rng F holds
Sum (LS * F) = 0
let F be FinSequence of S; ::_thesis: ( Carrier LS misses rng F implies Sum (LS * F) = 0 )
assume A1: Carrier LS misses rng F ; ::_thesis: Sum (LS * F) = 0
set LF = LS * F;
set LF0 = (len (LS * F)) |-> 0;
A2: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(LS_*_F)_holds_
(LS_*_F)_._k_=_((len_(LS_*_F))_|->_0)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len (LS * F) implies (LS * F) . k = ((len (LS * F)) |-> 0) . k )
assume A3: ( 1 <= k & k <= len (LS * F) ) ; ::_thesis: (LS * F) . k = ((len (LS * F)) |-> 0) . k
A4: k in dom (LS * F) by A3, FINSEQ_3:25;
then  k in dom F by FUNCT_1:11;
then  F . k in rng F by FUNCT_1:def_3;
then A5: ( dom LS = the carrier of S & not F . k in Carrier LS ) by A1, FUNCT_2:def_1, XBOOLE_0:3;
 ( (LS * F) . k = LS . (F . k) & F . k in dom LS ) by A4, FUNCT_1:11, FUNCT_1:12;
hence  (LS * F) . k = ((len (LS * F)) |-> 0) . k by A5; ::_thesis: verum
end;
 len ((len (LS * F)) |-> 0) = len (LS * F) by CARD_1:def_7;
then  LS * F = (len (LS * F)) |-> 0 by A2, FINSEQ_1:14;
hence  Sum (LS * F) = 0 by RVSUM_1:81; ::_thesis: verum
end;

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 & Carrier LS c= rng F holds
sum LS = Sum (LS * F)
proof
let S be non empty addLoopStr ; ::_thesis: for LS being Linear_Combination of S
for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds
sum LS = Sum (LS * F)
let LS be Linear_Combination of S; ::_thesis: for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds
sum LS = Sum (LS * F)
let F be FinSequence of S; ::_thesis: ( F is one-to-one & Carrier LS c= rng F implies sum LS = Sum (LS * F) )
assume that
A1: F is one-to-one and
A2: Carrier LS c= rng F ; ::_thesis: sum LS = Sum (LS * F)
consider G being FinSequence of S such that
A3: G is one-to-one and
A4: rng G = Carrier LS and
A5: sum LS = Sum (LS * G) by Def3;
reconsider R = rng G as Subset of (rng F) by A2, A4;
reconsider FR = F - R, FR1 = F - (R `) as FinSequence of S by FINSEQ_3:86;
consider p being Permutation of (dom F) such that
A6: F * p = (F - (R `)) ^ (F - R) by FINSEQ_3:115;
(rng F) \ (R `) = (R `) `
.= R ;
then A7: rng FR1 = R by FINSEQ_3:65;
 FR1 is one-to-one by A1, FINSEQ_3:87;
then  FR1,G are_fiberwise_equipotent by A3, A7, RFINSEQ:26;
then consider q being Permutation of (dom G) such that
A8: FR1 = G * q by RFINSEQ:4;
 len (LS * G) = len G by FINSEQ_2:33;
then A9: dom G = dom (LS * G) by FINSEQ_3:29;
 (LS * G) * q = LS * FR1 by A8, RELAT_1:36;
then A10: sum LS = Sum (LS * FR1) by A5, A9, FINSOP_1:7;
 len (LS * F) = len F by FINSEQ_2:33;
then A11: dom F = dom (LS * F) by FINSEQ_3:29;
 (rng F) \ R = rng FR by FINSEQ_3:65;
then  rng FR misses Carrier LS by A4, XBOOLE_1:79;
then A12: ( LS * (FR1 ^ FR) = (LS * FR1) ^ (LS * FR) & Sum (LS * FR) = 0 ) by Th29, FINSEQOP:9;
 (LS * F) * p = LS * (FR1 ^ FR) by A6, RELAT_1:36;
hence  Sum (LS * F) = Sum (LS * (FR1 ^ FR)) by A11, FINSOP_1:7
.= (sum LS) + 0 by A10, A12, RVSUM_1:75
.= sum LS ;
::_thesis: verum
end;

theorem Th31: :: RLAFFIN1:31
for S being non empty addLoopStr holds sum (ZeroLC S) = 0
proof
let S be non empty addLoopStr ; ::_thesis: sum (ZeroLC S) = 0
consider F being FinSequence of S such that
 F is one-to-one and
A1: rng F = Carrier (ZeroLC S) and
A2: sum (ZeroLC S) = Sum ((ZeroLC S) * F) by Def3;
 F = {} by A1, RLVECT_2:def_5;
hence  sum (ZeroLC S) = 0 by A2, RVSUM_1:72; ::_thesis: verum
end;

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
proof
let S be non empty addLoopStr ; ::_thesis: for LS being Linear_Combination of S
for v being Element of S st Carrier LS c= {v} holds
sum LS = LS . v
let LS be Linear_Combination of S; ::_thesis: for v being Element of S st Carrier LS c= {v} holds
sum LS = LS . v
let v be Element of S; ::_thesis: ( Carrier LS c= {v} implies sum LS = LS . v )
consider p being FinSequence such that
A1: rng p = {v} and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of S by A1, FINSEQ_1:def_4;
 ( dom LS = the carrier of S & p = <*v*> ) by A1, A2, FINSEQ_3:97, FUNCT_2:def_1;
then A3: LS * p = <*(LS . v)*> by FINSEQ_2:34;
assume  Carrier LS c= {v} ; ::_thesis: sum LS = LS . v
hence  sum LS = Sum (LS * p) by A1, A2, Th30
.= LS . v by A3, RVSUM_1:73 ;
::_thesis: verum
end;

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} & v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
proof
let S be non empty addLoopStr ; ::_thesis: for LS being Linear_Combination of S
for v1, v2 being Element of S st Carrier LS c= {v1,v2} & v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
let LS be Linear_Combination of S; ::_thesis: for v1, v2 being Element of S st Carrier LS c= {v1,v2} & v1 <> v2 holds
sum LS = (LS . v1) + (LS . v2)
let v1, v2 be Element of S; ::_thesis: ( Carrier LS c= {v1,v2} & v1 <> v2 implies sum LS = (LS . v1) + (LS . v2) )
consider p being FinSequence such that
A1: rng p = {v1,v2} and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of S by A1, FINSEQ_1:def_4;
assume that
A3: Carrier LS c= {v1,v2} and
A4: v1 <> v2 ; ::_thesis: sum LS = (LS . v1) + (LS . v2)
A5: dom LS = the carrier of S by FUNCT_2:def_1;
A6: Sum <*(LS . v1)*> = LS . v1 by RVSUM_1:73;
 ( p = <*v1,v2*> or p = <*v2,v1*> ) by A1, A2, A4, FINSEQ_3:99;
then  ( LS * p = <*(LS . v1),(LS . v2)*> or LS * p = <*(LS . v2),(LS . v1)*> ) by A5, FINSEQ_2:125;
then  ( Sum (LS * p) = (LS . v1) + (LS . v2) or Sum (LS * p) = (LS . v2) + (LS . v1) ) by A6, RVSUM_1:74, RVSUM_1:76;
hence  sum LS = (LS . v1) + (LS . v2) by A1, A2, A3, Th30; ::_thesis: verum
end;

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)
proof
let S be non empty addLoopStr ; ::_thesis: for LS1, LS2 being Linear_Combination of S holds sum (LS1 + LS2) = (sum LS1) + (sum LS2)
let LS1, LS2 be Linear_Combination of S; ::_thesis: sum (LS1 + LS2) = (sum LS1) + (sum LS2)
set C1 = Carrier LS1;
set C2 = Carrier LS2;
consider p112 being FinSequence such that
A1: rng p112 = (Carrier LS1) \ (Carrier LS2) and
A2: p112 is one-to-one by FINSEQ_4:58;
consider p12 being FinSequence such that
A3: rng p12 = (Carrier LS1) /\ (Carrier LS2) and
A4: p12 is one-to-one by FINSEQ_4:58;
consider p211 being FinSequence such that
A5: rng p211 = (Carrier LS2) \ (Carrier LS1) and
A6: p211 is one-to-one by FINSEQ_4:58;
reconsider p112 = p112, p12 = p12, p211 = p211 as FinSequence of S by A1, A3, A5, FINSEQ_1:def_4;
 (Carrier LS1) \ (Carrier LS2) misses (Carrier LS1) /\ (Carrier LS2) by XBOOLE_1:89;
then A7: p112 ^ p12 is one-to-one by A1, A2, A3, A4, FINSEQ_3:91;
set p1 = p112 ^ p12;
A8: rng (p112 ^ p12) = ((Carrier LS1) \ (Carrier LS2)) \/ ((Carrier LS1) /\ (Carrier LS2)) by A1, A3, FINSEQ_1:31
.= Carrier LS1 by XBOOLE_1:51 ;
then A9: rng ((p112 ^ p12) ^ p211) = (Carrier LS1) \/ ((Carrier LS2) \ (Carrier LS1)) by A5, FINSEQ_1:31
.= (Carrier LS1) \/ (Carrier LS2) by XBOOLE_1:39 ;
set p2 = p12 ^ p211;
A10: rng (p12 ^ p211) = ((Carrier LS1) /\ (Carrier LS2)) \/ ((Carrier LS2) \ (Carrier LS1)) by A3, A5, FINSEQ_1:31
.= Carrier LS2 by XBOOLE_1:51 ;
set pp = (p112 ^ p12) ^ p211;
 (p112 ^ p12) ^ p211 = p112 ^ (p12 ^ p211) by FINSEQ_1:32;
then A11: LS2 * ((p112 ^ p12) ^ p211) = (LS2 * p112) ^ (LS2 * (p12 ^ p211)) by FINSEQOP:9;
 (Carrier LS2) \ (Carrier LS1) misses (Carrier LS1) /\ (Carrier LS2) by XBOOLE_1:89;
then A12: p12 ^ p211 is one-to-one by A3, A4, A5, A6, FINSEQ_3:91;
 Carrier LS2 misses (Carrier LS1) \ (Carrier LS2) by XBOOLE_1:79;
then  Sum (LS2 * p112) = 0 by A1, Th29;
then A13: Sum (LS2 * ((p112 ^ p12) ^ p211)) = 0 + (Sum (LS2 * (p12 ^ p211))) by A11, RVSUM_1:75
.= sum LS2 by A10, A12, Def3 ;
 ( len (LS1 * ((p112 ^ p12) ^ p211)) = len ((p112 ^ p12) ^ p211) & len (LS2 * ((p112 ^ p12) ^ p211)) = len ((p112 ^ p12) ^ p211) ) by FINSEQ_2:33;
then reconsider L1p = LS1 * ((p112 ^ p12) ^ p211), L2p = LS2 * ((p112 ^ p12) ^ p211) as Element of (len ((p112 ^ p12) ^ p211)) -tuples_on REAL by FINSEQ_2:92;
A14: (LS1 + LS2) * ((p112 ^ p12) ^ p211) = L1p + L2p by Th13;
A15: Carrier LS1 misses (Carrier LS2) \ (Carrier LS1) by XBOOLE_1:79;
then  ( LS1 * ((p112 ^ p12) ^ p211) = (LS1 * (p112 ^ p12)) ^ (LS1 * p211) & Sum (LS1 * p211) = 0 ) by A5, Th29, FINSEQOP:9;
then A16: Sum (LS1 * ((p112 ^ p12) ^ p211)) = (Sum (LS1 * (p112 ^ p12))) + 0 by RVSUM_1:75
.= sum LS1 by A7, A8, Def3 ;
A17: Carrier (LS1 + LS2) c= (Carrier LS1) \/ (Carrier LS2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (LS1 + LS2) or x in (Carrier LS1) \/ (Carrier LS2) )
assume  x in Carrier (LS1 + LS2) ; ::_thesis: x in (Carrier LS1) \/ (Carrier LS2)
then consider u being Element of S such that
A18: x = u and
A19: (LS1 + LS2) . u <> 0 ;
 (LS1 + LS2) . u = (LS1 . u) + (LS2 . u) by RLVECT_2:def_10;
then  ( LS1 . u <> 0 or LS2 . u <> 0 ) by A19;
then  ( x in Carrier LS1 or x in Carrier LS2 ) by A18;
hence  x in (Carrier LS1) \/ (Carrier LS2) by XBOOLE_0:def_3; ::_thesis: verum
end;
 (p112 ^ p12) ^ p211 is one-to-one by A5, A6, A7, A8, A15, FINSEQ_3:91;
hence  sum (LS1 + LS2) = Sum (L1p + L2p) by A9, A14, A17, Th30
.= (sum LS1) + (sum LS2) by A13, A16, RVSUM_1:89 ;
::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds sum (r * L) = r * (sum L)
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds sum (r * L) = r * (sum L)
let L be Linear_Combination of V; ::_thesis: sum (r * L) = r * (sum L)
consider F being FinSequence of V such that
A1: F is one-to-one and
A2: rng F = Carrier L and
A3: sum L = Sum (L * F) by Def3;
 L is Linear_Combination of Carrier L by RLVECT_2:def_6;
then  r * L is Linear_Combination of Carrier L by RLVECT_2:44;
then A4: Carrier (r * L) c= rng F by A2, RLVECT_2:def_6;
thus r * (sum L) = Sum (r * (L * F)) by A3, RVSUM_1:87
.= Sum ((r * L) * F) by Th14
.= sum (r * L) by A1, A4, Th30 ; ::_thesis: verum
end;

theorem Th36: :: RLAFFIN1:36
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds sum (L1 - L2) = (sum L1) - (sum L2)
proof
let V be RealLinearSpace; ::_thesis: for L1, L2 being Linear_Combination of V holds sum (L1 - L2) = (sum L1) - (sum L2)
let L1, L2 be Linear_Combination of V; ::_thesis: sum (L1 - L2) = (sum L1) - (sum L2)
thus  sum (L1 - L2) = (sum L1) + (sum ((- 1) * L2)) by Th34
.= (sum L1) + ((- 1) * (sum L2)) by Th35
.= (sum L1) - (sum L2) ; ::_thesis: verum
end;

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)
proof
let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for LG being Linear_Combination of G
for g being Element of G holds sum LG = sum (g + LG)
let LG be Linear_Combination of G; ::_thesis: for g being Element of G holds sum LG = sum (g + LG)
let g be Element of G; ::_thesis: sum LG = sum (g + LG)
set gL = g + LG;
deffunc H1( Element of G) ->  Element of the carrier of G = $1 + g;
consider f being Function of the carrier of G, the carrier of G such that
A1: for h being Element of G holds f . h = H1(h) from FUNCT_2:sch_4();
consider F being FinSequence of G such that
A2: F is one-to-one and
A3: rng F = Carrier LG and
A4: sum LG = Sum (LG * F) by Def3;
A5: len (f * F) = len F by FINSEQ_2:33;
A6: len (LG * F) = len F by FINSEQ_2:33;
A7: len ((g + LG) * (f * F)) = len (f * F) by FINSEQ_2:33;
A8: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_F_holds_
((g_+_LG)_*_(f_*_F))_._k_=_(LG_*_F)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len F implies ((g + LG) * (f * F)) . k = (LG * F) . k )
assume A9: ( 1 <= k & k <= len F ) ; ::_thesis: ((g + LG) * (f * F)) . k = (LG * F) . k
then  k in dom F by FINSEQ_3:25;
then A10: F /. k = F . k by PARTFUN1:def_6;
 k in dom (LG * F) by A6, A9, FINSEQ_3:25;
then A11: (LG * F) . k = LG . (F . k) by FUNCT_1:12;
 k in dom ((g + LG) * (f * F)) by A5, A7, A9, FINSEQ_3:25;
then A12: ((g + LG) * (f * F)) . k = (g + LG) . ((f * F) . k) by FUNCT_1:12;
 k in dom (f * F) by A5, A9, FINSEQ_3:25;
then  (f * F) . k = f . (F . k) by FUNCT_1:12;
then  (f * F) . k = (F /. k) + g by A1, A10;
hence ((g + LG) * (f * F)) . k = LG . (((F /. k) + g) - g) by A12, Def1
.= LG . (((F /. k) + g) + (- g)) by RLVECT_1:def_11
.= LG . ((F /. k) + (g + (- g))) by RLVECT_1:def_3
.= LG . ((F /. k) + (0. G)) by RLVECT_1:def_10
.= (LG * F) . k by A10, A11, RLVECT_1:4 ;
::_thesis: verum
end;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(f_*_F)_&_x2_in_dom_(f_*_F)_&_(f_*_F)_._x1_=_(f_*_F)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 implies x1 = x2 )
assume that
A13: x1 in dom (f * F) and
A14: x2 in dom (f * F) and
A15: (f * F) . x1 = (f * F) . x2 ; ::_thesis: x1 = x2
A16: f . (F /. x1) = (F /. x1) + g by A1;
A17: x1 in dom F by A13, FUNCT_1:11;
then A18: F . x1 = F /. x1 by PARTFUN1:def_6;
A19: x2 in dom F by A14, FUNCT_1:11;
then A20: F . x2 = F /. x2 by PARTFUN1:def_6;
 ( (f * F) . x1 = f . (F . x1) & (f * F) . x2 = f . (F . x2) ) by A13, A14, FUNCT_1:12;
then  (F /. x1) + g = (F /. x2) + g by A1, A15, A16, A18, A20;
then  F /. x1 = F /. x2 by RLVECT_1:8;
hence  x1 = x2 by A2, A17, A18, A19, A20, FUNCT_1:def_4; ::_thesis: verum
end;
then A21: f * F is one-to-one by FUNCT_1:def_4;
 Carrier (g + LG) c= rng (f * F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (g + LG) or x in rng (f * F) )
assume  x in Carrier (g + LG) ; ::_thesis: x in rng (f * F)
then  x in g + (Carrier LG) by Th16;
then consider h being Element of G such that
A22: x = g + h and
A23: h in Carrier LG ;
consider y being set  such that
A24: y in dom F and
A25: F . y = h by A3, A23, FUNCT_1:def_3;
A26: f . (F . y) = x by A1, A22, A25;
 dom f = the carrier of G by FUNCT_2:def_1;
then A27: y in dom (f * F) by A24, A25, FUNCT_1:11;
then  (f * F) . y in rng (f * F) by FUNCT_1:def_3;
hence  x in rng (f * F) by A26, A27, FUNCT_1:12; ::_thesis: verum
end;
then  sum (g + LG) = Sum ((g + LG) * (f * F)) by A21, Th30;
hence  sum LG = sum (g + LG) by A4, A5, A6, A7, A8, FINSEQ_1:14; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: 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)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for LR being Linear_Combination of R st r <> 0 holds
sum LR = sum (r (*) LR)
let LR be Linear_Combination of R; ::_thesis: ( r <> 0 implies sum LR = sum (r (*) LR) )
set rL = r (*) LR;
deffunc H1( Element of R) ->  Element of the carrier of R = r * $1;
consider f being Function of the carrier of R, the carrier of R such that
A1: for v being Element of R holds f . v = H1(v) from FUNCT_2:sch_4();
consider F being FinSequence of R such that
A2: F is one-to-one and
A3: rng F = Carrier LR and
A4: sum LR = Sum (LR * F) by Def3;
assume A5: r <> 0 ; ::_thesis: sum LR = sum (r (*) LR)
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(f_*_F)_&_x2_in_dom_(f_*_F)_&_(f_*_F)_._x1_=_(f_*_F)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 implies x1 = x2 )
assume that
A6: x1 in dom (f * F) and
A7: x2 in dom (f * F) and
A8: (f * F) . x1 = (f * F) . x2 ; ::_thesis: x1 = x2
A9: f . (F /. x1) = r * (F /. x1) by A1;
A10: x1 in dom F by A6, FUNCT_1:11;
then A11: F . x1 = F /. x1 by PARTFUN1:def_6;
A12: x2 in dom F by A7, FUNCT_1:11;
then A13: F . x2 = F /. x2 by PARTFUN1:def_6;
 ( (f * F) . x1 = f . (F . x1) & (f * F) . x2 = f . (F . x2) ) by A6, A7, FUNCT_1:12;
then A14: r * (F /. x1) = r * (F /. x2) by A1, A8, A9, A11, A13;
F /. x1 = 1 * (F /. x1) by RLVECT_1:def_8
.= ((r ") * r) * (F /. x1) by A5, XCMPLX_0:def_7
.= (r ") * (r * (F /. x2)) by A14, RLVECT_1:def_7
.= ((r ") * r) * (F /. x2) by RLVECT_1:def_7
.= 1 * (F /. x2) by A5, XCMPLX_0:def_7
.= F /. x2 by RLVECT_1:def_8 ;
hence  x1 = x2 by A2, A10, A11, A12, A13, FUNCT_1:def_4; ::_thesis: verum
end;
then A15: f * F is one-to-one by FUNCT_1:def_4;
A16: len (LR * F) = len F by FINSEQ_2:33;
A17: len (f * F) = len F by FINSEQ_2:33;
A18: len ((r (*) LR) * (f * F)) = len (f * F) by FINSEQ_2:33;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_F_holds_
((r_(*)_LR)_*_(f_*_F))_._k_=_(LR_*_F)_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len F implies ((r (*) LR) * (f * F)) . k = (LR * F) . k )
assume A19: ( 1 <= k & k <= len F ) ; ::_thesis: ((r (*) LR) * (f * F)) . k = (LR * F) . k
then  k in dom F by FINSEQ_3:25;
then A20: F /. k = F . k by PARTFUN1:def_6;
 k in dom (LR * F) by A16, A19, FINSEQ_3:25;
then A21: (LR * F) . k = LR . (F . k) by FUNCT_1:12;
 k in dom (f * F) by A17, A19, FINSEQ_3:25;
then A22: (f * F) . k = f . (F . k) by FUNCT_1:12;
 k in dom ((r (*) LR) * (f * F)) by A17, A18, A19, FINSEQ_3:25;
then  ((r (*) LR) * (f * F)) . k = (r (*) LR) . ((f * F) . k) by FUNCT_1:12;
hence ((r (*) LR) * (f * F)) . k = (r (*) LR) . (r * (F /. k)) by A1, A20, A22
.= LR . ((r ") * (r * (F /. k))) by A5, Def2
.= LR . (((r ") * r) * (F /. k)) by RLVECT_1:def_7
.= LR . (1 * (F /. k)) by A5, XCMPLX_0:def_7
.= (LR * F) . k by A20, A21, RLVECT_1:def_8 ;
::_thesis: verum
end;
then A23: LR * F = (r (*) LR) * (f * F) by A16, A17, A18, FINSEQ_1:14;
 Carrier (r (*) LR) c= rng (f * F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier (r (*) LR) or x in rng (f * F) )
assume  x in Carrier (r (*) LR) ; ::_thesis: x in rng (f * F)
then  x in r * (Carrier LR) by A5, Th23;
then consider v being Element of R such that
A24: x = r * v and
A25: v in Carrier LR ;
consider y being set  such that
A26: y in dom F and
A27: F . y = v by A3, A25, FUNCT_1:def_3;
A28: f . v = x by A1, A24;
A29: dom F = dom (f * F) by A17, FINSEQ_3:29;
then  (f * F) . y = f . v by A26, A27, FUNCT_1:12;
hence  x in rng (f * F) by A26, A28, A29, FUNCT_1:def_3; ::_thesis: verum
end;
hence  sum LR = sum (r (*) LR) by A4, A15, A23, Th30; ::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)
let v be VECTOR of V; ::_thesis: for L being Linear_Combination of V holds Sum (v + L) = ((sum L) * v) + (Sum L)
let L be Linear_Combination of V; ::_thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
defpred S1[ Nat] means  for L being Linear_Combination of V st card (Carrier L) <= $1 holds
Sum (v + L) = ((sum L) * v) + (Sum L);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let L be Linear_Combination of V; ::_thesis: ( card (Carrier L) <= n + 1 implies Sum (v + L) = ((sum L) * v) + (Sum L) )
assume A3: card (Carrier L) <= n + 1 ; ::_thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
percases ( card (Carrier L) <= n or card (Carrier L) = n + 1 ) by A3, NAT_1:8;
suppose card (Carrier L) <= n ; ::_thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
hence  Sum (v + L) = ((sum L) * v) + (Sum L) by A2; ::_thesis: verum
end;
supposeA4: card (Carrier L) = n + 1 ; ::_thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
then  not Carrier L is empty ;
then consider w being set  such that
A5: w in Carrier L by XBOOLE_0:def_1;
reconsider w = w as Element of V by A5;
A6: card ((Carrier L) \ {w}) = n by A4, A5, STIRL2_1:55;
consider Lw being Linear_Combination of {w} such that
A7: Lw . w = L . w by RLVECT_4:37;
set LLw = L - Lw;
(L - Lw) . w = (L . w) - (Lw . w) by RLVECT_2:54
.= 0 by A7 ;
then A8: not w in Carrier (L - Lw) by RLVECT_2:19;
A9: Carrier Lw c= {w} by RLVECT_2:def_6;
then A10: ( Carrier (L - Lw) c= (Carrier L) \/ (Carrier Lw) & (Carrier L) \/ (Carrier Lw) c= (Carrier L) \/ {w} ) by RLVECT_2:55, XBOOLE_1:9;
 (Carrier L) \/ {w} = Carrier L by A5, ZFMISC_1:40;
then  Carrier (L - Lw) c= Carrier L by A10, XBOOLE_1:1;
then  card (Carrier (L - Lw)) <= n by A8, A6, NAT_1:43, ZFMISC_1:34;
then A11: Sum (v + (L - Lw)) = ((sum (L - Lw)) * v) + (Sum (L - Lw)) by A2;
A12: (L - Lw) + Lw = L + (Lw - Lw) by RLVECT_2:40
.= L + (ZeroLC V) by RLVECT_2:57
.= L by RLVECT_2:41 ;
then A13: Sum L = (Sum (L - Lw)) + (Sum Lw) by RLVECT_3:1
.= (Sum (L - Lw)) + ((Lw . w) * w) by RLVECT_2:32 ;
 v + (Carrier Lw) c= v + {w} by A9, RLTOPSP1:8;
then  v + (Carrier Lw) c= {(v + w)} by Lm3;
then  Carrier (v + Lw) c= {(v + w)} by Th16;
then  v + Lw is Linear_Combination of {(v + w)} by RLVECT_2:def_6;
then A14: Sum (v + Lw) = ((v + Lw) . (v + w)) * (v + w) by RLVECT_2:32
.= (Lw . ((v + w) - v)) * (v + w) by Def1
.= (Lw . w) * (v + w) by RLVECT_4:1 ;
A15: sum L = (sum (L - Lw)) + (sum Lw) by A12, Th34
.= (sum (L - Lw)) + (Lw . w) by A9, Th32 ;
 v + L = (v + (L - Lw)) + (v + Lw) by A12, Th17;
hence  Sum (v + L) = (Sum (v + (L - Lw))) + (Sum (v + Lw)) by RLVECT_3:1
.= (((sum (L - Lw)) * v) + (Sum (L - Lw))) + (((Lw . w) * v) + ((Lw . w) * w)) by A11, A14, RLVECT_1:def_5
.= ((((sum (L - Lw)) * v) + (Sum (L - Lw))) + ((Lw . w) * v)) + ((Lw . w) * w) by RLVECT_1:def_3
.= ((((sum (L - Lw)) * v) + ((Lw . w) * v)) + (Sum (L - Lw))) + ((Lw . w) * w) by RLVECT_1:def_3
.= (((sum L) * v) + (Sum (L - Lw))) + ((Lw . w) * w) by A15, RLVECT_1:def_6
.= ((sum L) * v) + (Sum L) by A13, RLVECT_1:def_3 ;
::_thesis: verum
end;
end;
end;
A16: S1[ 0 ]
proof
let L be Linear_Combination of V; ::_thesis: ( card (Carrier L) <= 0 implies Sum (v + L) = ((sum L) * v) + (Sum L) )
assume  card (Carrier L) <= 0 ; ::_thesis: Sum (v + L) = ((sum L) * v) + (Sum L)
then A17: Carrier L = {} V ;
then A18: ( L = ZeroLC V & Sum L = 0. V ) by RLVECT_2:34, RLVECT_2:def_5;
 v + (Carrier L) = {} by A17, Th8;
then  Carrier (v + L) = {} by Th16;
hence  Sum (v + L) = 0. V by RLVECT_2:34
.= (0. V) + (0. V) by RLVECT_1:4
.= ((sum L) * v) + (Sum L) by A18, Th31, RLVECT_1:10 ;
::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A16, A1);
then  S1[ card (Carrier L)] ;
hence  Sum (v + L) = ((sum L) * v) + (Sum L) ; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds Sum (r (*) L) = r * (Sum L)
let L be Linear_Combination of V; ::_thesis: Sum (r (*) L) = r * (Sum L)
defpred S1[ Nat] means  for L being Linear_Combination of V st card (Carrier L) <= $1 holds
Sum (r (*) L) = r * (Sum L);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let L be Linear_Combination of V; ::_thesis: ( card (Carrier L) <= n + 1 implies Sum (r (*) L) = r * (Sum L) )
assume A3: card (Carrier L) <= n + 1 ; ::_thesis: Sum (r (*) L) = r * (Sum L)
percases ( r = 0 or r <> 0 ) ;
suppose r = 0 ; ::_thesis: Sum (r (*) L) = r * (Sum L)
then  ( r (*) L = ZeroLC V & r * (Sum L) = 0. V ) by Def2, RLVECT_1:10;
hence  Sum (r (*) L) = r * (Sum L) by RLVECT_2:30; ::_thesis: verum
end;
supposeA4: r <> 0 ; ::_thesis: Sum (r (*) L) = r * (Sum L)
percases ( card (Carrier L) <= n or card (Carrier L) = n + 1 ) by A3, NAT_1:8;
suppose card (Carrier L) <= n ; ::_thesis: Sum (r (*) L) = r * (Sum L)
hence  Sum (r (*) L) = r * (Sum L) by A2; ::_thesis: verum
end;
supposeA5: card (Carrier L) = n + 1 ; ::_thesis: Sum (r (*) L) = r * (Sum L)
then  Carrier L <> {} ;
then consider p being set  such that
A6: p in Carrier L by XBOOLE_0:def_1;
reconsider p = p as Element of V by A6;
A7: card ((Carrier L) \ {p}) = n by A5, A6, STIRL2_1:55;
consider Lp being Linear_Combination of {p} such that
A8: Lp . p = L . p by RLVECT_4:37;
set LLp = L - Lp;
(L - Lp) . p = (L . p) - (Lp . p) by RLVECT_2:54
.= 0 by A8 ;
then A9: not p in Carrier (L - Lp) by RLVECT_2:19;
A10: Carrier Lp c= {p} by RLVECT_2:def_6;
then A11: ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (Carrier L) \/ {p} ) by RLVECT_2:55, XBOOLE_1:9;
 r * (Carrier Lp) c= {(r * p)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (Carrier Lp) or x in {(r * p)} )
assume  x in r * (Carrier Lp) ; ::_thesis: x in {(r * p)}
then consider w being Element of V such that
A12: x = r * w and
A13: w in Carrier Lp ;
 w = p by A10, A13, TARSKI:def_1;
hence  x in {(r * p)} by A12, TARSKI:def_1; ::_thesis: verum
end;
then  Carrier (r (*) Lp) c= {(r * p)} by A4, Th23;
then  r (*) Lp is Linear_Combination of {(r * p)} by RLVECT_2:def_6;
then A14: Sum (r (*) Lp) = ((r (*) Lp) . (r * p)) * (r * p) by RLVECT_2:32
.= (Lp . ((r ") * (r * p))) * (r * p) by A4, Def2
.= (Lp . (((r ") * r) * p)) * (r * p) by RLVECT_1:def_7
.= (Lp . (1 * p)) * (r * p) by A4, XCMPLX_0:def_7
.= (Lp . p) * (r * p) by RLVECT_1:def_8 ;
A15: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40
.= L + (ZeroLC V) by RLVECT_2:57
.= L by RLVECT_2:41 ;
then A16: Sum L = (Sum (L - Lp)) + (Sum Lp) by RLVECT_3:1
.= (Sum (L - Lp)) + ((Lp . p) * p) by RLVECT_2:32 ;
 (Carrier L) \/ {p} = Carrier L by A6, ZFMISC_1:40;
then  Carrier (L - Lp) c= Carrier L by A11, XBOOLE_1:1;
then  card (Carrier (L - Lp)) <= n by A9, A7, NAT_1:43, ZFMISC_1:34;
then A17: Sum (r (*) (L - Lp)) = r * (Sum (L - Lp)) by A2;
 r (*) L = (r (*) (L - Lp)) + (r (*) Lp) by A15, Th24;
hence  Sum (r (*) L) = (Sum (r (*) (L - Lp))) + (Sum (r (*) Lp)) by RLVECT_3:1
.= (r * (Sum (L - Lp))) + (((Lp . p) * r) * p) by A14, A17, RLVECT_1:def_7
.= (r * (Sum (L - Lp))) + (r * ((Lp . p) * p)) by RLVECT_1:def_7
.= r * (Sum L) by A16, RLVECT_1:def_5 ;
::_thesis: verum
end;
end;
end;
end;
end;
A18: S1[ 0 ]
proof
let L be Linear_Combination of V; ::_thesis: ( card (Carrier L) <= 0 implies Sum (r (*) L) = r * (Sum L) )
assume  card (Carrier L) <= 0 ; ::_thesis: Sum (r (*) L) = r * (Sum L)
then  Carrier L = {} ;
then A19: L = ZeroLC V by RLVECT_2:def_5;
then  ( r * (0. V) = 0. V & Sum L = 0. V ) by RLVECT_1:10, RLVECT_2:30;
hence  Sum (r (*) L) = r * (Sum L) by A19, Th26; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A18, A1);
then  S1[ card (Carrier L)] ;
hence  Sum (r (*) L) = r * (Sum L) ; ::_thesis: verum
end;

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 & ((- 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 & ((- 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
proof
 {v} is affinely-independent
proof
assume  not {v} is empty ; :: according to RLAFFIN1:def_4 ::_thesis: ex v being VECTOR of V st
( v in {v} & ((- v) + {v}) \ {(0. V)} is linearly-independent )
take  v ; ::_thesis: ( v in {v} & ((- v) + {v}) \ {(0. V)} is linearly-independent )
thus  v in {v} by TARSKI:def_1; ::_thesis: ((- v) + {v}) \ {(0. V)} is linearly-independent
 (- v) + v = 0. V by RLVECT_1:5;
then  (- v) + {v} = {(0. V)} by Lm3;
then  ((- v) + {v}) \ {(0. V)} = {} the carrier of V by XBOOLE_1:37;
hence  ((- v) + {v}) \ {(0. V)} is linearly-independent by RLVECT_3:7; ::_thesis: verum
end;
hence  for b1 being Subset of V st b1 = {v} holds
b1 is affinely-independent ; ::_thesis: verum
end;
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
proof
percases ( v = w or v <> w ) ;
suppose v = w ; ::_thesis: for b1 being Subset of V st b1 = {v,w} holds
b1 is affinely-independent
then  {v,w} = {w} by ENUMSET1:29;
hence  for b1 being Subset of V st b1 = {v,w} holds
b1 is affinely-independent ; ::_thesis: verum
end;
supposeA1: v <> w ; ::_thesis: for b1 being Subset of V st b1 = {v,w} holds
b1 is affinely-independent
 (- v) + {v,w} c= {((- v) + w),(0. V)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- v) + {v,w} or x in {((- v) + w),(0. V)} )
assume  x in (- v) + {v,w} ; ::_thesis: x in {((- v) + w),(0. V)}
then consider r being Element of V such that
A2: x = (- v) + r and
A3: r in {v,w} ;
percases ( r = v or r = w ) by A3, TARSKI:def_2;
suppose r = v ; ::_thesis: x in {((- v) + w),(0. V)}
then  x = 0. V by A2, RLVECT_1:5;
hence  x in {((- v) + w),(0. V)} by TARSKI:def_2; ::_thesis: verum
end;
suppose r = w ; ::_thesis: x in {((- v) + w),(0. V)}
hence  x in {((- v) + w),(0. V)} by A2, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
then A4: ((- v) + {v,w}) \ {(0. V)} c= {((- v) + w),(0. V)} \ {(0. V)} by XBOOLE_1:33;
 - (- v) = v by RLVECT_1:17;
then A5: w + (- v) <> 0. V by A1, RLVECT_1:6;
then A6: {((- v) + w)} is linearly-independent by RLVECT_3:8;
 {v,w} is affinely-independent
proof
assume  not {v,w} is empty ; :: according to RLAFFIN1:def_4 ::_thesis: ex v being VECTOR of V st
( v in {v,w} & ((- v) + {v,w}) \ {(0. V)} is linearly-independent )
take  v ; ::_thesis: ( v in {v,w} & ((- v) + {v,w}) \ {(0. V)} is linearly-independent )
thus  v in {v,w} by TARSKI:def_2; ::_thesis: ((- v) + {v,w}) \ {(0. V)} is linearly-independent
 ( 0. V in {(0. V)} & not (- v) + w in {(0. V)} ) by A5, TARSKI:def_1;
then  ((- v) + {v,w}) \ {(0. V)} c= {((- v) + w)} by A4, ZFMISC_1:62;
hence  ((- v) + {v,w}) \ {(0. V)} is linearly-independent by A6, RLVECT_3:5; ::_thesis: verum
end;
hence  for b1 being Subset of V st b1 = {v,w} holds
b1 is affinely-independent ; ::_thesis: verum
end;
end;
end;
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 & b1 is affinely-independent )
proof
take  { the Element of V} ; ::_thesis: ( { the Element of V} is 1 -element & { the Element of V} is affinely-independent )
thus  ( { the Element of V} is 1 -element & { the Element of V} is affinely-independent ) ; ::_thesis: verum
end;
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 & sum L = 0 holds
Carrier L = {}
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st A is affinely-independent holds
for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
let A be Subset of V; ::_thesis: ( A is affinely-independent implies for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
assume A1: A is affinely-independent ; ::_thesis: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {}
let L be Linear_Combination of A; ::_thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )
assume that
A2: Sum L = 0. V and
A3: sum L = 0 ; ::_thesis: Carrier L = {}
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: Carrier L = {}
then  Carrier L c= {} by RLVECT_2:def_6;
hence  Carrier L = {} ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: Carrier L = {}
then consider p being VECTOR of V such that
A4: p in A and
A5: ((- p) + A) \ {(0. V)} is linearly-independent by A1, Def4;
A6: A \/ {p} = A by A4, ZFMISC_1:40;
consider Lp being Linear_Combination of {p} such that
A7: Lp . p = L . p by RLVECT_4:37;
set LLp = L - Lp;
((- p) + (L - Lp)) . (0. V) = (L - Lp) . ((0. V) - (- p)) by Def1
.= (L - Lp) . (- (- p)) by RLVECT_1:14
.= (L - Lp) . p by RLVECT_1:17
.= (L . p) - (Lp . p) by RLVECT_2:54
.= 0 by A7 ;
then A8: not 0. V in Carrier ((- p) + (L - Lp)) by RLVECT_2:19;
A9: Carrier Lp c= {p} by RLVECT_2:def_6;
then A10: ( Carrier Lp = {p} or Carrier Lp = {} ) by ZFMISC_1:33;
 Carrier L c= A by RLVECT_2:def_6;
then  ( Carrier (L - Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= A \/ {p} ) by A9, RLVECT_2:55, XBOOLE_1:13;
then A11: Carrier (L - Lp) c= A by A6, XBOOLE_1:1;
 Carrier ((- p) + (L - Lp)) = (- p) + (Carrier (L - Lp)) by Th16;
then  Carrier ((- p) + (L - Lp)) c= (- p) + A by A11, RLTOPSP1:8;
then  Carrier ((- p) + (L - Lp)) c= ((- p) + A) \ {(0. V)} by A8, ZFMISC_1:34;
then A12: (- p) + (L - Lp) is Linear_Combination of ((- p) + A) \ {(0. V)} by RLVECT_2:def_6;
A13: (L - Lp) + Lp = L + (Lp - Lp) by RLVECT_2:40
.= L + (ZeroLC V) by RLVECT_2:57
.= L by RLVECT_2:41 ;
A14: Sum ((- p) + Lp) = ((sum Lp) * (- p)) + (Sum Lp) by Th39
.= ((sum Lp) * (- p)) + ((Lp . p) * p) by RLVECT_2:32
.= ((Lp . p) * (- p)) + ((Lp . p) * p) by A9, Th32
.= (Lp . p) * ((- p) + p) by RLVECT_1:def_5
.= (Lp . p) * (0. V) by RLVECT_1:5
.= 0. V by RLVECT_1:10 ;
Sum ((- p) + L) = ((sum L) * (- p)) + (Sum L) by Th39
.= (0. V) + (0. V) by A2, A3, RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then  0. V = Sum (((- p) + (L - Lp)) + ((- p) + Lp)) by A13, Th17
.= (Sum ((- p) + (L - Lp))) + (0. V) by A14, RLVECT_3:1
.= Sum ((- p) + (L - Lp)) by RLVECT_1:4 ;
then  {} = Carrier ((- p) + (L - Lp)) by A5, A12, RLVECT_3:def_1;
then A15: ZeroLC V = (- p) + (L - Lp) by RLVECT_2:def_5;
A16: L - Lp = (0. V) + (L - Lp) by Th21
.= (p + (- p)) + (L - Lp) by RLVECT_1:5
.= p + ((- p) + (L - Lp)) by Th19
.= ZeroLC V by A15, Th20 ;
then  sum (L - Lp) = 0 by Th31;
then  0 = 0 + (sum Lp) by A3, A13, Th34
.= 0 + (Lp . p) by A9, Th32 ;
then  not p in Carrier Lp by RLVECT_2:19;
then  (Carrier (L - Lp)) \/ (Carrier Lp) = {} by A10, A16, RLVECT_2:def_5, TARSKI:def_1;
then  Carrier L c= {} by A13, RLVECT_2:37;
hence  Carrier L = {} ; ::_thesis: verum
end;
end;
end;

Lm6:  for V being RealLinearSpace
for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & 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
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st ( for L being Linear_Combination of A st Sum L = 0. V & 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
let A be Subset of V; ::_thesis: ( ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) implies for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent )
assume A1: for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ; ::_thesis: for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent
let p be Element of V; ::_thesis: ( p in A implies ((- p) + A) \ {(0. V)} is linearly-independent )
assume A2: p in A ; ::_thesis: ((- p) + A) \ {(0. V)} is linearly-independent
set pA = (- p) + A;
set pA0 = ((- p) + A) \ {(0. V)};
 (- p) + p = 0. V by RLVECT_1:5;
then  0. V in (- p) + A by A2;
then A3: (((- p) + A) \ {(0. V)}) \/ {(0. V)} = (- p) + A by ZFMISC_1:116;
let L be Linear_Combination of ((- p) + A) \ {(0. V)}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum L = 0. V or Carrier L = {} )
assume A4: Sum L = 0. V ; ::_thesis: Carrier L = {}
reconsider sL = - (sum L) as Real ;
consider Lp being Linear_Combination of {(0. V)} such that
A5: Lp . (0. V) = sL by RLVECT_4:37;
set LLp = L + Lp;
set pLLp = p + (L + Lp);
A6: Carrier Lp c= {(0. V)} by RLVECT_2:def_6;
A7: p + ((- p) + A) = (p + (- p)) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
A8: Carrier (p + (L + Lp)) = p + (Carrier (L + Lp)) by Th16;
A9: Carrier L c= ((- p) + A) \ {(0. V)} by RLVECT_2:def_6;
then  ( Carrier (L + Lp) c= (Carrier L) \/ (Carrier Lp) & (Carrier L) \/ (Carrier Lp) c= (((- p) + A) \ {(0. V)}) \/ {(0. V)} ) by A6, RLVECT_2:37, XBOOLE_1:13;
then  Carrier (L + Lp) c= (- p) + A by A3, XBOOLE_1:1;
then  Carrier (p + (L + Lp)) c= A by A7, A8, RLTOPSP1:8;
then A10: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def_6;
A11: sum (p + (L + Lp)) = sum (L + Lp) by Th37;
A12: sum (L + Lp) = (sum L) + (sum Lp) by Th34
.= (sum L) + sL by A5, A6, Th32
.= 0 ;
then  Sum (p + (L + Lp)) = (0 * p) + (Sum (L + Lp)) by Th39
.= (0. V) + (Sum (L + Lp)) by RLVECT_1:10
.= Sum (L + Lp) by RLVECT_1:4
.= (Sum L) + (Sum Lp) by RLVECT_3:1
.= Sum Lp by A4, RLVECT_1:4
.= (Lp . (0. V)) * (0. V) by RLVECT_2:32
.= 0. V by RLVECT_1:10 ;
then  Carrier (p + (L + Lp)) = {} by A1, A10, A11, A12;
then A13: p + (L + Lp) = ZeroLC V by RLVECT_2:def_5;
A14: L + Lp = (0. V) + (L + Lp) by Th21
.= ((- p) + p) + (L + Lp) by RLVECT_1:5
.= (- p) + (ZeroLC V) by A13, Th19
.= ZeroLC V by Th20 ;
assume  Carrier L <> {} ; ::_thesis: contradiction
then consider v being set  such that
A15: v in Carrier L by XBOOLE_0:def_1;
reconsider v = v as Element of V by A15;
 not v in Carrier Lp by A6, A9, A15, XBOOLE_0:def_5;
then  Lp . v = 0 ;
then (L . v) + 0 = (L + Lp) . v by RLVECT_2:def_10
.= 0 by A14, RLVECT_2:20 ;
hence  contradiction by A15, RLVECT_2:19; ::_thesis: verum
end;

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 )
proof
let V be RealLinearSpace; ::_thesis: 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 )
let A be Subset of V; ::_thesis: ( A is affinely-independent iff for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent )
hereby  ::_thesis: ( ( for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent ) implies A is affinely-independent )
assume  A is affinely-independent ; ::_thesis: for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent
then  for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} by Lm5;
hence  for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent by Lm6; ::_thesis: verum
end;
assume A1: for v being VECTOR of V st v in A holds
((- v) + A) \ {(0. V)} is linearly-independent ; ::_thesis: A is affinely-independent
assume  not A is empty ; :: according to RLAFFIN1:def_4 ::_thesis: ex v being VECTOR of V st
( v in A & ((- v) + A) \ {(0. V)} is linearly-independent )
then consider v being set  such that
A2: v in A by XBOOLE_0:def_1;
reconsider v = v as Element of V by A2;
take  v ; ::_thesis: ( v in A & ((- v) + A) \ {(0. V)} is linearly-independent )
thus  ( v in A & ((- v) + A) \ {(0. V)} is linearly-independent ) by A1, A2; ::_thesis: verum
end;

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 & sum L = 0 holds
Carrier L = {} )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds
( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
let A be Subset of V; ::_thesis: ( A is affinely-independent iff for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} )
thus  ( A is affinely-independent implies for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) by Lm5; ::_thesis: ( ( for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ) implies A is affinely-independent )
assume  for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} ; ::_thesis: A is affinely-independent
then  for p being VECTOR of V st p in A holds
((- p) + A) \ {(0. V)} is linearly-independent by Lm6;
hence  A is affinely-independent by Th41; ::_thesis: verum
end;

theorem Th43: :: RLAFFIN1:43
for V being RealLinearSpace
for A, B being Subset of V st A is affinely-independent & B c= A holds
B is affinely-independent
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st A is affinely-independent & B c= A holds
B is affinely-independent
let A, B be Subset of V; ::_thesis: ( A is affinely-independent & B c= A implies B is affinely-independent )
assume that
A1: A is affinely-independent and
A2: B c= A ; ::_thesis: B is affinely-independent
now__::_thesis:_for_L_being_Linear_Combination_of_B_st_Sum_L_=_0._V_&_sum_L_=_0_holds_
Carrier_L_=_{}
let L be Linear_Combination of B; ::_thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )
assume A3: ( Sum L = 0. V & sum L = 0 ) ; ::_thesis: Carrier L = {}
 L is Linear_Combination of A by A2, RLVECT_2:21;
hence  Carrier L = {} by A1, A3, Th42; ::_thesis: verum
end;
hence  B is affinely-independent by Th42; ::_thesis: verum
end;

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
proof
let A be Subset of V; ::_thesis: ( A is linearly-independent implies A is affinely-independent )
assume  A is linearly-independent ; ::_thesis: A is affinely-independent
then  for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds
Carrier L = {} by RLVECT_3:def_1;
hence  A is affinely-independent by Th42; ::_thesis: verum
end;
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
proof
set vI = v + I;
now__::_thesis:_for_L_being_Linear_Combination_of_v_+_I_st_Sum_L_=_0._V_&_sum_L_=_0_holds_
Carrier_L_=_{}
let L be Linear_Combination of v + I; ::_thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )
assume that
A1: Sum L = 0. V and
A2: sum L = 0 ; ::_thesis: Carrier L = {}
set vL = (- v) + L;
A3: sum ((- v) + L) = 0 by A2, Th37;
A4: ( Carrier ((- v) + L) = (- v) + (Carrier L) & Carrier L c= v + I ) by Th16, RLVECT_2:def_6;
(- v) + (v + I) = ((- v) + v) + I by Th5
.= (0. V) + I by RLVECT_1:5
.= I by Th6 ;
then  Carrier ((- v) + L) c= I by A4, RLTOPSP1:8;
then A5: (- v) + L is Linear_Combination of I by RLVECT_2:def_6;
Sum ((- v) + L) = (0 * (- v)) + (0. V) by A1, A2, Th39
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
then  Carrier ((- v) + L) = {} by A3, A5, Th42;
then A6: (- v) + L = ZeroLC V by RLVECT_2:def_5;
L = (0. V) + L by Th21
.= (v + (- v)) + L by RLVECT_1:5
.= v + (ZeroLC V) by A6, Th19
.= ZeroLC V by Th20 ;
hence  Carrier L = {} by RLVECT_2:def_5; ::_thesis: verum
end;
hence  v + I is affinely-independent by Th42; ::_thesis: verum
end;
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
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for A being Subset of V st v + A is affinely-independent holds
A is affinely-independent
let v be VECTOR of V; ::_thesis: for A being Subset of V st v + A is affinely-independent holds
A is affinely-independent
let A be Subset of V; ::_thesis: ( v + A is affinely-independent implies A is affinely-independent )
assume A1: v + A is affinely-independent ; ::_thesis: A is affinely-independent
(- v) + (v + A) = ((- v) + v) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
hence  A is affinely-independent by A1; ::_thesis: verum
end;

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
proof
percases ( r = 0 or r <> 0 ) ;
suppose r = 0 ; ::_thesis: r * I is affinely-independent
then  r * I c= {(0. V)} by Th12;
then  ( r * I = {} V or r * I = {(0. V)} ) by ZFMISC_1:33;
hence  r * I is affinely-independent ; ::_thesis: verum
end;
supposeA1: r <> 0 ; ::_thesis: r * I is affinely-independent
now__::_thesis:_for_L_being_Linear_Combination_of_r_*_I_st_Sum_L_=_0._V_&_sum_L_=_0_holds_
Carrier_L_=_{}
let L be Linear_Combination of r * I; ::_thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )
assume that
A2: Sum L = 0. V and
A3: sum L = 0 ; ::_thesis: Carrier L = {}
set rL = (r ") (*) L;
A4: Sum ((r ") (*) L) = (r ") * (0. V) by A2, Th40
.= 0. V by RLVECT_1:10 ;
A5: ( Carrier ((r ") (*) L) = (r ") * (Carrier L) & Carrier L c= r * I ) by A1, Th23, RLVECT_2:def_6;
(r ") * (r * I) = ((r ") * r) * I by Th10
.= 1 * I by A1, XCMPLX_0:def_7
.= I by Th11 ;
then  Carrier ((r ") (*) L) c= I by A5, Th9;
then A6: (r ") (*) L is Linear_Combination of I by RLVECT_2:def_6;
 sum ((r ") (*) L) = 0 by A1, A3, Th38;
then  Carrier ((r ") (*) L) = {} by A4, A6, Th42;
then A7: (r ") (*) L = ZeroLC V by RLVECT_2:def_5;
L = 1 (*) L by Th28
.= (r * (r ")) (*) L by A1, XCMPLX_0:def_7
.= r (*) (ZeroLC V) by A7, Th27
.= ZeroLC V by Th26 ;
hence  Carrier L = {} by RLVECT_2:def_5; ::_thesis: verum
end;
hence  r * I is affinely-independent by Th42; ::_thesis: verum
end;
end;
end;
end;

theorem :: RLAFFIN1:45
for r being Real
for V being RealLinearSpace
for A being Subset of V st r * A is affinely-independent & r <> 0 holds
A is affinely-independent
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for A being Subset of V st r * A is affinely-independent & r <> 0 holds
A is affinely-independent
let V be RealLinearSpace; ::_thesis: for A being Subset of V st r * A is affinely-independent & r <> 0 holds
A is affinely-independent
let A be Subset of V; ::_thesis: ( r * A is affinely-independent & r <> 0 implies A is affinely-independent )
assume that
A1: r * A is affinely-independent and
A2: r <> 0 ; ::_thesis: A is affinely-independent
(r ") * (r * A) = ((r ") * r) * A by Th10
.= 1 * A by A2, XCMPLX_0:def_7
.= A by Th11 ;
hence  A is affinely-independent by A1; ::_thesis: verum
end;

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 )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V st 0. V in A holds
( A is affinely-independent iff A \ {(0. V)} is linearly-independent )
let A be Subset of V; ::_thesis: ( 0. V in A implies ( A is affinely-independent iff A \ {(0. V)} is linearly-independent ) )
assume A1: 0. V in A ; ::_thesis: ( A is affinely-independent iff A \ {(0. V)} is linearly-independent )
A2: (- (0. V)) + A = (0. V) + A by RLVECT_1:12
.= A by Th6 ;
hence  ( A is affinely-independent implies A \ {(0. V)} is linearly-independent ) by A1, Th41; ::_thesis: ( A \ {(0. V)} is linearly-independent implies A is affinely-independent )
assume  A \ {(0. V)} is linearly-independent ; ::_thesis: A is affinely-independent
hence  A is affinely-independent by A1, A2, Def4; ::_thesis: verum
end;

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
proof
let F be Subset-Family of V; ::_thesis: ( F is empty implies F is affinely-independent )
assume A1: F is empty ; ::_thesis: F is affinely-independent
let A be Subset of V; :: according to RLAFFIN1:def_5 ::_thesis: ( A in F implies A is affinely-independent )
assume  A in F ; ::_thesis: A is affinely-independent
hence  A is affinely-independent by A1; ::_thesis: verum
end;
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
proof
 for A being Subset of V st A in {I} holds
A is affinely-independent by TARSKI:def_1;
hence  for b1 being Subset-Family of V st b1 = {I} holds
b1 is affinely-independent by Def5; ::_thesis: verum
end;
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 & b1 is affinely-independent )
proof
take  {} (bool the carrier of V) ; ::_thesis: ( {} (bool the carrier of V) is empty & {} (bool the carrier of V) is affinely-independent )
thus  ( {} (bool the carrier of V) is empty & {} (bool the carrier of V) is affinely-independent ) ; ::_thesis: verum
end;
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 & b1 is affinely-independent )
proof
take  { the affinely-independent Subset of V} ; ::_thesis: ( not { the affinely-independent Subset of V} is empty & { the affinely-independent Subset of V} is affinely-independent )
thus  ( not { the affinely-independent Subset of V} is empty & { the affinely-independent Subset of V} is affinely-independent ) ; ::_thesis: verum
end;
end;

theorem :: RLAFFIN1:47
for V being RealLinearSpace
for F1, F2 being Subset-Family of V st F1 is affinely-independent & F2 is affinely-independent holds
F1 \/ F2 is affinely-independent
proof
let V be RealLinearSpace; ::_thesis: for F1, F2 being Subset-Family of V st F1 is affinely-independent & F2 is affinely-independent holds
F1 \/ F2 is affinely-independent
let F1, F2 be Subset-Family of V; ::_thesis: ( F1 is affinely-independent & F2 is affinely-independent implies F1 \/ F2 is affinely-independent )
assume A1: ( F1 is affinely-independent & F2 is affinely-independent ) ; ::_thesis: F1 \/ F2 is affinely-independent
let A be Subset of V; :: according to RLAFFIN1:def_5 ::_thesis: ( A in F1 \/ F2 implies A is affinely-independent )
assume  A in F1 \/ F2 ; ::_thesis: A is affinely-independent
then  ( A in F1 or A in F2 ) by XBOOLE_0:def_3;
hence  A is affinely-independent by A1, Def5; ::_thesis: verum
end;

theorem :: RLAFFIN1:48
for V being RealLinearSpace
for F1, F2 being Subset-Family of V st F1 c= F2 & F2 is affinely-independent holds
F1 is affinely-independent
proof
let V be RealLinearSpace; ::_thesis: for F1, F2 being Subset-Family of V st F1 c= F2 & F2 is affinely-independent holds
F1 is affinely-independent
let F1, F2 be Subset-Family of V; ::_thesis: ( F1 c= F2 & F2 is affinely-independent implies F1 is affinely-independent )
assume A1: ( F1 c= F2 & F2 is affinely-independent ) ; ::_thesis: F1 is affinely-independent
let A be Subset of V; :: according to RLAFFIN1:def_5 ::_thesis: ( A in F1 implies A is affinely-independent )
assume  A in F1 ; ::_thesis: A is affinely-independent
hence  A is affinely-independent by A1, Def5; ::_thesis: verum
end;

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
proof
set BB =  {  B where B is Affine Subset of RLS : A c= B  }  ;
  {  B where B is Affine Subset of RLS : A c= B  }  c= bool ([#] RLS)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  B where B is Affine Subset of RLS : A c= B  }  or x in bool ([#] RLS) )
assume  x in  {  B where B is Affine Subset of RLS : A c= B  }  ; ::_thesis: x in bool ([#] RLS)
then  ex B being Affine Subset of RLS st
( x = B & A c= B ) ;
hence  x in bool ([#] RLS) ; ::_thesis: verum
end;
then reconsider BB =  {  B where B is Affine Subset of RLS : A c= B  }  as Subset-Family of RLS ;
 meet BB is Subset of RLS ;
hence  meet  {  B where B is Affine Subset of RLS : A c= B  }  is Subset of RLS ; ::_thesis: verum
end;
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
proof
set BB =  {  B where B is Affine Subset of RLS : A c= B  }  ;
let v1, v2 be Element of RLS; :: according to RUSUB_4:def_4 ::_thesis: for b1 being Element of REAL holds
( not v1 in Affin A or not v2 in Affin A or ((1 - b1) * v1) + (b1 * v2) in Affin A )
let r be Real; ::_thesis: ( not v1 in Affin A or not v2 in Affin A or ((1 - r) * v1) + (r * v2) in Affin A )
assume that
A1: v1 in Affin A and
A2: v2 in Affin A ; ::_thesis: ((1 - r) * v1) + (r * v2) in Affin A
A3: now__::_thesis:_for_Y_being_set_st_Y_in__{__B_where_B_is_Affine_Subset_of_RLS_:_A_c=_B__}__holds_
((1_-_r)_*_v1)_+_(r_*_v2)_in_Y
let Y be set ; ::_thesis: ( Y in  {  B where B is Affine Subset of RLS : A c= B  }  implies ((1 - r) * v1) + (r * v2) in Y )
assume A4: Y in  {  B where B is Affine Subset of RLS : A c= B  }  ; ::_thesis: ((1 - r) * v1) + (r * v2) in Y
then consider B being Affine Subset of RLS such that
A5: Y = B and
 A c= B ;
 ( v1 in B & v2 in B ) by A1, A2, A4, A5, SETFAM_1:def_1;
hence  ((1 - r) * v1) + (r * v2) in Y by A5, RUSUB_4:def_4; ::_thesis: verum
end;
  {  B where B is Affine Subset of RLS : A c= B  }  <> {} by A1, SETFAM_1:def_1;
hence  ((1 - r) * v1) + (r * v2) in Affin A by A3, SETFAM_1:def_1; ::_thesis: verum
end;
end;

Lm7:  for V being non empty RLSStruct
for A being Subset of V holds A c= Affin A
proof
let V be non empty RLSStruct ; ::_thesis: for A being Subset of V holds A c= Affin A
let A be Subset of V; ::_thesis: A c= Affin A
set BB =  {  B where B is Affine Subset of V : A c= B  }  ;
A1: now__::_thesis:_for_Y_being_set_st_Y_in__{__B_where_B_is_Affine_Subset_of_V_:_A_c=_B__}__holds_
A_c=_Y
let Y be set ; ::_thesis: ( Y in  {  B where B is Affine Subset of V : A c= B  }  implies A c= Y )
assume  Y in  {  B where B is Affine Subset of V : A c= B  }  ; ::_thesis: A c= Y
then  ex B being Affine Subset of V st
( Y = B & A c= B ) ;
hence  A c= Y ; ::_thesis: verum
end;
 [#] V is Affine by RUSUB_4:22;
then  [#] V in  {  B where B is Affine Subset of V : A c= B  }  ;
hence  A c= Affin A by A1, SETFAM_1:5; ::_thesis: verum
end;

Lm8:  for V being non empty RLSStruct
for A being Affine Subset of V holds A = Affin A
proof
let V be non empty RLSStruct ; ::_thesis: for A being Affine Subset of V holds A = Affin A
let A be Affine Subset of V; ::_thesis: A = Affin A
set BB =  {  B where B is Affine Subset of V : A c= B  }  ;
 A in  {  B where B is Affine Subset of V : A c= B  }  ;
then A1: Affin A c= A by SETFAM_1:3;
 A c= Affin A by Lm7;
hence  A = Affin A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let RLS be non empty RLSStruct ;
let A be empty Subset of RLS;
cluster Affin A ->  empty ;
coherence
 Affin A is empty
proof
 {} RLS is Affine by RUSUB_4:22;
hence  Affin A is empty by Lm8; ::_thesis: verum
end;
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
proof
 A c= Affin A by Lm7;
hence  not Affin A is empty ; ::_thesis: verum
end;
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 & B is Affine holds
Affin A c= B
proof
let RLS be non empty RLSStruct ; ::_thesis: for A, B being Subset of RLS st A c= B & B is Affine holds
Affin A c= B
let A, B be Subset of RLS; ::_thesis: ( A c= B & B is Affine implies Affin A c= B )
assume  ( A c= B & B is Affine ) ; ::_thesis: Affin A c= B
then  B in  {  C where C is Affine Subset of RLS : A c= C  }  ;
hence  Affin A c= B by SETFAM_1:3; ::_thesis: verum
end;

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
proof
let RLS be non empty RLSStruct ; ::_thesis: for A, B being Subset of RLS st A c= B holds
Affin A c= Affin B
let A, B be Subset of RLS; ::_thesis: ( A c= B implies Affin A c= Affin B )
assume A1: A c= B ; ::_thesis: Affin A c= Affin B
 B c= Affin B by Lm7;
then  A c= Affin B by A1, XBOOLE_1:1;
hence  Affin A c= Affin B by Th51; ::_thesis: verum
end;

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)
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for A being Subset of V holds Affin (v + A) = v + (Affin A)
let v be VECTOR of V; ::_thesis: for A being Subset of V holds Affin (v + A) = v + (Affin A)
let A be Subset of V; ::_thesis: Affin (v + A) = v + (Affin A)
 v + A c= v + (Affin A) by Lm7, RLTOPSP1:8;
then A1: Affin (v + A) c= v + (Affin A) by Th51, RUSUB_4:31;
(- v) + (v + A) = ((- v) + v) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
then  A c= (- v) + (Affin (v + A)) by Lm7, RLTOPSP1:8;
then A2: Affin A c= (- v) + (Affin (v + A)) by Th51, RUSUB_4:31;
v + ((- v) + (Affin (v + A))) = (v + (- v)) + (Affin (v + A)) by Th5
.= (0. V) + (Affin (v + A)) by RLVECT_1:5
.= Affin (v + A) by Th6 ;
then  v + (Affin A) c= Affin (v + A) by A2, RLTOPSP1:8;
hence  Affin (v + A) = v + (Affin A) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

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
proof
let r be Real; ::_thesis: 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
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for AR being Subset of R st AR is Affine holds
r * AR is Affine
let AR be Subset of R; ::_thesis: ( AR is Affine implies r * AR is Affine )
assume A1: AR is Affine ; ::_thesis: r * AR is Affine
let v1, v2 be VECTOR of R; :: according to RUSUB_4:def_4 ::_thesis: for b1 being Element of REAL holds
( not v1 in r * AR or not v2 in r * AR or ((1 - b1) * v1) + (b1 * v2) in r * AR )
let s be Real; ::_thesis: ( not v1 in r * AR or not v2 in r * AR or ((1 - s) * v1) + (s * v2) in r * AR )
assume  v1 in r * AR ; ::_thesis: ( not v2 in r * AR or ((1 - s) * v1) + (s * v2) in r * AR )
then consider w1 being Element of R such that
A2: v1 = r * w1 and
A3: w1 in AR ;
assume  v2 in r * AR ; ::_thesis: ((1 - s) * v1) + (s * v2) in r * AR
then consider w2 being Element of R such that
A4: v2 = r * w2 and
A5: w2 in AR ;
A6: ((1 - s) * w1) + (s * w2) in AR by A1, A3, A5, RUSUB_4:def_4;
A7: (1 - s) * (r * w1) = ((1 - s) * r) * w1 by RLVECT_1:def_7
.= r * ((1 - s) * w1) by RLVECT_1:def_7 ;
s * (r * w2) = (s * r) * w2 by RLVECT_1:def_7
.= r * (s * w2) by RLVECT_1:def_7 ;
then  ((1 - s) * v1) + (s * v2) = r * (((1 - s) * w1) + (s * w2)) by A2, A4, A7, RLVECT_1:def_5;
hence  ((1 - s) * v1) + (s * v2) in r * AR by A6; ::_thesis: verum
end;

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)
proof
let r be Real; ::_thesis: 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)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; ::_thesis: for AR being Subset of R st r <> 0 holds
Affin (r * AR) = r * (Affin AR)
let AR be Subset of R; ::_thesis: ( r <> 0 implies Affin (r * AR) = r * (Affin AR) )
assume A1: r <> 0 ; ::_thesis: Affin (r * AR) = r * (Affin AR)
(r ") * (r * AR) = ((r ") * r) * AR by Th10
.= 1 * AR by A1, XCMPLX_0:def_7
.= AR by Th11 ;
then  AR c= (r ") * (Affin (r * AR)) by Lm7, Th9;
then A2: Affin AR c= (r ") * (Affin (r * AR)) by Th51, Th54;
 r * AR c= r * (Affin AR) by Lm7, Th9;
then A3: Affin (r * AR) c= r * (Affin AR) by Th51, Th54;
r * ((r ") * (Affin (r * AR))) = (r * (r ")) * (Affin (r * AR)) by Th10
.= 1 * (Affin (r * AR)) by A1, XCMPLX_0:def_7
.= Affin (r * AR) by Th11 ;
then  r * (Affin AR) c= Affin (r * AR) by A2, Th9;
hence  Affin (r * AR) = r * (Affin AR) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: RLAFFIN1:56
for r being Real
for V being RealLinearSpace
for A being Subset of V holds Affin (r * A) = r * (Affin A)
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for A being Subset of V holds Affin (r * A) = r * (Affin A)
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Affin (r * A) = r * (Affin A)
let A be Subset of V; ::_thesis: Affin (r * A) = r * (Affin A)
percases ( r = 0 or r <> 0 ) ;
supposeA1: r = 0 ; ::_thesis: Affin (r * A) = r * (Affin A)
then A2: r * (Affin A) c= {(0. V)} by Th12;
A3: r * (Affin A) c= r * A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (Affin A) or x in r * A )
assume A4: x in r * (Affin A) ; ::_thesis: x in r * A
then  ex v being Element of V st
( x = r * v & v in Affin A ) ;
then  not A is empty ;
then consider v being set  such that
A5: v in A by XBOOLE_0:def_1;
reconsider v = v as Element of V by A5;
A6: r * v in r * A by A5;
 x = 0. V by A2, A4, TARSKI:def_1;
hence  x in r * A by A1, A6, RLVECT_1:10; ::_thesis: verum
end;
 r * A c= {(0. V)} by A1, Th12;
then A7: ( r * A is empty or r * A = {(0. V)} ) by ZFMISC_1:33;
 {(0. V)} is Affine by RUSUB_4:23;
then A8: Affin (r * A) = r * A by A7, Lm8;
 r * A c= r * (Affin A) by Lm7, Th9;
hence  Affin (r * A) = r * (Affin A) by A3, A8, XBOOLE_0:def_10; ::_thesis: verum
end;
suppose r <> 0 ; ::_thesis: Affin (r * A) = r * (Affin A)
hence  Affin (r * A) = r * (Affin A) by Th55; ::_thesis: verum
end;
end;
end;

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)))
proof
let V be RealLinearSpace; ::_thesis: 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)))
let v be VECTOR of V; ::_thesis: for A being Subset of V st v in Affin A holds
Affin A = v + (Up (Lin ((- v) + A)))
let A be Subset of V; ::_thesis: ( v in Affin A implies Affin A = v + (Up (Lin ((- v) + A))) )
set vA = (- v) + A;
set BB =  {  B where B is Affine Subset of V : (- v) + A c= B  }  ;
A1: (- v) + A c= Up (Lin ((- v) + A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- v) + A or x in Up (Lin ((- v) + A)) )
assume  x in (- v) + A ; ::_thesis: x in Up (Lin ((- v) + A))
then  x in Lin ((- v) + A) by RLVECT_3:15;
hence  x in Up (Lin ((- v) + A)) by STRUCT_0:def_5; ::_thesis: verum
end;
 Up (Lin ((- v) + A)) is Affine by RUSUB_4:24;
then A2: Up (Lin ((- v) + A)) in  {  B where B is Affine Subset of V : (- v) + A c= B  }  by A1;
then A3: Affin ((- v) + A) c= Up (Lin ((- v) + A)) by SETFAM_1:3;
assume  v in Affin A ; ::_thesis: Affin A = v + (Up (Lin ((- v) + A)))
then  (- v) + v in (- v) + (Affin A) ;
then A4: 0. V in (- v) + (Affin A) by RLVECT_1:5;
now__::_thesis:_for_Y_being_set_st_Y_in__{__B_where_B_is_Affine_Subset_of_V_:_(-_v)_+_A_c=_B__}__holds_
Up_(Lin_((-_v)_+_A))_c=_Y
let Y be set ; ::_thesis: ( Y in  {  B where B is Affine Subset of V : (- v) + A c= B  }  implies Up (Lin ((- v) + A)) c= Y )
A5: Affin ((- v) + A) = (- v) + (Affin A) by Th53;
assume  Y in  {  B where B is Affine Subset of V : (- v) + A c= B  }  ; ::_thesis: Up (Lin ((- v) + A)) c= Y
then consider B being Affine Subset of V such that
A6: Y = B and
A7: (- v) + A c= B ;
A8: Lin ((- v) + A) is Subspace of Lin B by A7, RLVECT_3:20;
 Affin ((- v) + A) c= B by A7, Th51;
then  B = the carrier of (Lin B) by A4, A5, RUSUB_4:26;
hence  Up (Lin ((- v) + A)) c= Y by A6, A8, RLSUB_1:def_2; ::_thesis: verum
end;
then  Up (Lin ((- v) + A)) c= Affin ((- v) + A) by A2, SETFAM_1:5;
then  Up (Lin ((- v) + A)) = Affin ((- v) + A) by A3, XBOOLE_0:def_10;
hence v + (Up (Lin ((- v) + A))) = v + ((- v) + (Affin A)) by Th53
.= (v + (- v)) + (Affin A) by Th5
.= (0. V) + (Affin A) by RLVECT_1:5
.= Affin A by Th6 ;
::_thesis: verum
end;

Lm9:  for V being RealLinearSpace
for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Lin (A \/ {(0. V)}) = Lin A
let A be Subset of V; ::_thesis: Lin (A \/ {(0. V)}) = Lin A
 {(0. V)} = the carrier of ((0). V) by RLSUB_1:def_3;
then  Lin {(0. V)} = (0). V by RLVECT_3:18;
hence  Lin (A \/ {(0. V)}) = (Lin A) + ((0). V) by RLVECT_3:22
.= Lin A by RLSUB_2:9 ;
::_thesis: verum
end;

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 & Affin A = Affin B holds
A = B )
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds
( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds
A = B )
let A be Subset of V; ::_thesis: ( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds
A = B )
hereby  ::_thesis: ( ( for B being Subset of V st B c= A & Affin A = Affin B holds
A = B ) implies A is affinely-independent )
assume A1: A is affinely-independent ; ::_thesis: for B being Subset of V st B c= A & Affin A = Affin B holds
not A <> B
let B be Subset of V; ::_thesis: ( B c= A & Affin A = Affin B implies not A <> B )
assume that
A2: B c= A and
A3: Affin A = Affin B ; ::_thesis: not A <> B
assume  A <> B ; ::_thesis: contradiction
then  B c< A by A2, XBOOLE_0:def_8;
then consider p being set  such that
A4: p in A and
A5: not p in B by XBOOLE_0:6;
reconsider p = p as Element of V by A4;
A6: A \ {p} c= Affin (A \ {p}) by Lm7;
 not B is empty by A3, A4;
then consider q being set  such that
A7: q in B by XBOOLE_0:def_1;
reconsider q = q as Element of V by A7;
 - (- q) = q by RLVECT_1:17;
then A8: (- q) + p <> 0. V by A5, A7, RLVECT_1:def_10;
set qA0 = ((- q) + A) \ {(0. V)};
 (- q) + p in (- q) + A by A4;
then A9: (- q) + p in ((- q) + A) \ {(0. V)} by A8, ZFMISC_1:56;
 ((- q) + A) \ {(0. V)} is linearly-independent by A1, A2, A7, Th41;
then A10: not (- q) + p in Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}) by A9, RLVECT_5:17;
A11: q + ((- q) + p) = (q + (- q)) + p by RLVECT_1:def_3
.= (0. V) + p by RLVECT_1:5
.= p by RLVECT_1:4 ;
 (- q) + q = 0. V by RLVECT_1:5;
then  0. V in (- q) + A by A2, A7;
then A12: 0. V in ((- q) + A) \ {((- q) + p)} by A8, ZFMISC_1:56;
(((- q) + A) \ {(0. V)}) \ {((- q) + p)} = ((- q) + A) \ ({(0. V)} \/ {((- q) + p)}) by XBOOLE_1:41
.= (((- q) + A) \ {((- q) + p)}) \ {(0. V)} by XBOOLE_1:41 ;
then A13: Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}) = Lin (((((- q) + A) \ {((- q) + p)}) \ {(0. V)}) \/ {(0. V)}) by Lm9
.= Lin (((- q) + A) \ {((- q) + p)}) by A12, ZFMISC_1:116
.= Lin (((- q) + A) \ ((- q) + {p})) by Lm3
.= Lin ((- q) + (A \ {p})) by Lm2 ;
 q in A \ {p} by A2, A5, A7, ZFMISC_1:56;
then A14: Affin (A \ {p}) = q + (Up (Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}))) by A6, A13, Th57;
A15: not p in Affin (A \ {p})
proof
assume  p in Affin (A \ {p}) ; ::_thesis: contradiction
then consider v being Element of V such that
A16: p = q + v and
A17: v in Up (Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)})) by A14;
 (- q) + p = v by A11, A16, RLVECT_1:8;
hence  contradiction by A10, A17, STRUCT_0:def_5; ::_thesis: verum
end;
 B c= A \ {p} by A2, A5, ZFMISC_1:34;
then A18: Affin B c= Affin (A \ {p}) by Th52;
 Affin (A \ {p}) c= Affin A by Th52, XBOOLE_1:36;
then A19: Affin A = Affin (A \ {p}) by A3, A18, XBOOLE_0:def_10;
 A c= Affin A by Lm7;
hence  contradiction by A4, A15, A19; ::_thesis: verum
end;
assume A20: for B being Subset of V st B c= A & Affin A = Affin B holds
A = B ; ::_thesis: A is affinely-independent
assume  not A is affinely-independent ; ::_thesis: contradiction
then consider p being Element of V such that
A21: p in A and
A22: not ((- p) + A) \ {(0. V)} is linearly-independent by Th41;
set L = Lin (((- p) + A) \ {(0. V)});
 ((- p) + A) \ {(0. V)} c= the carrier of (Lin (((- p) + A) \ {(0. V)}))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((- p) + A) \ {(0. V)} or x in the carrier of (Lin (((- p) + A) \ {(0. V)})) )
assume  x in ((- p) + A) \ {(0. V)} ; ::_thesis: x in the carrier of (Lin (((- p) + A) \ {(0. V)}))
then  x in Lin (((- p) + A) \ {(0. V)}) by RLVECT_3:15;
hence  x in the carrier of (Lin (((- p) + A) \ {(0. V)})) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider pA0 = ((- p) + A) \ {(0. V)} as Subset of (Lin (((- p) + A) \ {(0. V)})) ;
 (- p) + p = 0. V by RLVECT_1:5;
then A23: 0. V in (- p) + A by A21;
then A24: pA0 \/ {(0. V)} = (- p) + A by ZFMISC_1:116;
 Lin pA0 = Lin (((- p) + A) \ {(0. V)}) by RLVECT_5:20;
then consider b being Subset of (Lin (((- p) + A) \ {(0. V)})) such that
A25: b c= pA0 and
A26: b is linearly-independent and
A27: Lin b = Lin (((- p) + A) \ {(0. V)}) by RLVECT_3:25;
reconsider B = b as linearly-independent Subset of V by A26, RLVECT_5:14;
A28: B \/ {(0. V)} c= pA0 \/ {(0. V)} by A25, XBOOLE_1:9;
 0. V in {(0. V)} by TARSKI:def_1;
then  ( p + (0. V) = p & 0. V in B \/ {(0. V)} ) by RLVECT_1:4, XBOOLE_0:def_3;
then A29: p in p + (B \/ {(0. V)}) ;
A30: p + (B \/ {(0. V)}) c= Affin (p + (B \/ {(0. V)})) by Lm7;
A31: p + ((- p) + A) = (p + (- p)) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
A32: (- p) + (p + (B \/ {(0. V)})) = ((- p) + p) + (B \/ {(0. V)}) by Th5
.= (0. V) + (B \/ {(0. V)}) by RLVECT_1:5
.= B \/ {(0. V)} by Th6 ;
 A c= Affin A by Lm7;
then  Affin A = p + (Up (Lin ((- p) + A))) by A21, Th57
.= p + (Up (Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}))) by A23, ZFMISC_1:116
.= p + (Up (Lin (((- p) + A) \ {(0. V)}))) by Lm9
.= p + (Up (Lin B)) by A27, RLVECT_5:20
.= p + (Up (Lin ((- p) + (p + (B \/ {(0. V)}))))) by A32, Lm9
.= Affin (p + (B \/ {(0. V)})) by A29, A30, Th57 ;
then pA0 = (B \/ {(0. V)}) \ {(0. V)} by A20, A24, A28, A31, A32, RLTOPSP1:8
.= B by RLVECT_3:6, ZFMISC_1:117 ;
hence  contradiction by A22; ::_thesis: verum
end;

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  }
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }
let A be Subset of V; ::_thesis: Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }
set S =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  ;
percases ( A is empty or not A is empty ) ;
supposeA1: A is empty ; ::_thesis: Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }
assume  Affin A <>  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  ; ::_thesis: contradiction
then  not  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  is empty by A1;
then consider x being set  such that
A2: x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  by XBOOLE_0:def_1;
consider L being Linear_Combination of A such that
 x = Sum L and
A3: sum L = 1 by A2;
 A = {} the carrier of V by A1;
then  L = ZeroLC V by RLVECT_2:23;
hence  contradiction by A3, Th31; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }
then consider p being set  such that
A4: p in A by XBOOLE_0:def_1;
reconsider p = p as Element of V by A4;
 A c= Affin A by Lm7;
then A5: Affin A = p + (Up (Lin ((- p) + A))) by A4, Th57;
thus  Affin A c=  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  c= Affin A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Affin A or x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  )
assume  x in Affin A ; ::_thesis: x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }
then consider v being VECTOR of V such that
A6: x = p + v and
A7: v in Up (Lin ((- p) + A)) by A5;
 v in Lin ((- p) + A) by A7, STRUCT_0:def_5;
then consider L being Linear_Combination of (- p) + A such that
A8: Sum L = v by RLVECT_3:14;
set pL = p + L;
consider Lp being Linear_Combination of {(0. V)} such that
A9: Lp . (0. V) = 1 - (sum L) by RLVECT_4:37;
set pLL = p + (L + Lp);
set pLp = p + Lp;
A10: Carrier Lp c= {(0. V)} by RLVECT_2:def_6;
then A11: p + (Carrier Lp) c= p + {(0. V)} by RLTOPSP1:8;
A12: ( Carrier (p + L) = p + (Carrier L) & Carrier L c= (- p) + A ) by Th16, RLVECT_2:def_6;
p + ((- p) + A) = (p + (- p)) + A by Th5
.= (0. V) + A by RLVECT_1:5
.= A by Th6 ;
then A13: Carrier (p + L) c= A by A12, RLTOPSP1:8;
A14: ( Carrier ((p + L) + (p + Lp)) c= (Carrier (p + L)) \/ (Carrier (p + Lp)) & p + (L + Lp) = (p + L) + (p + Lp) ) by Th17, RLVECT_2:37;
 ( Carrier (p + Lp) = p + (Carrier Lp) & p + {(0. V)} = {(p + (0. V))} ) by Lm3, Th16;
then  Carrier (p + Lp) c= {p} by A11, RLVECT_1:4;
then  (Carrier (p + L)) \/ (Carrier (p + Lp)) c= A \/ {p} by A13, XBOOLE_1:13;
then  Carrier (p + (L + Lp)) c= A \/ {p} by A14, XBOOLE_1:1;
then  Carrier (p + (L + Lp)) c= A by A4, ZFMISC_1:40;
then A15: p + (L + Lp) is Linear_Combination of A by RLVECT_2:def_6;
A16: sum (p + (L + Lp)) = sum (L + Lp) by Th37;
A17: sum (L + Lp) = (sum L) + (sum Lp) by Th34
.= (sum L) + (1 - (sum L)) by A9, A10, Th32
.= 1 ;
then  Sum (p + (L + Lp)) = (1 * p) + (Sum (L + Lp)) by Th39
.= (1 * p) + (v + (Sum Lp)) by A8, RLVECT_3:1
.= (1 * p) + (v + ((Lp . (0. V)) * (0. V))) by RLVECT_2:32
.= (1 * p) + (v + (0. V)) by RLVECT_1:10
.= p + (v + (0. V)) by RLVECT_1:def_8
.= x by A6, RLVECT_1:4 ;
hence  x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  by A15, A16, A17; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  or x in Affin A )
assume  x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  ; ::_thesis: x in Affin A
then consider L being Linear_Combination of A such that
A18: Sum L = x and
A19: sum L = 1 ;
set pL = (- p) + L;
 Carrier L c= A by RLVECT_2:def_6;
then A20: (- p) + (Carrier L) c= (- p) + A by RLTOPSP1:8;
 (- p) + (Carrier L) = Carrier ((- p) + L) by Th16;
then  (- p) + L is Linear_Combination of (- p) + A by A20, RLVECT_2:def_6;
then  Sum ((- p) + L) in Lin ((- p) + A) by RLVECT_3:14;
then A21: Sum ((- p) + L) in Up (Lin ((- p) + A)) by STRUCT_0:def_5;
p + (Sum ((- p) + L)) = p + ((1 * (- p)) + (Sum L)) by A19, Th39
.= p + ((- p) + (Sum L)) by RLVECT_1:def_8
.= (p + (- p)) + (Sum L) by RLVECT_1:def_3
.= (0. V) + (Sum L) by RLVECT_1:5
.= x by A18, RLVECT_1:4 ;
hence  x in Affin A by A5, A21; ::_thesis: verum
end;
end;
end;

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 & Ia c= A & Affin Ia = Affin A )
proof
let V be RealLinearSpace; ::_thesis: 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 & Ia c= A & Affin Ia = Affin A )
let A be Subset of V; ::_thesis: 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 & Ia c= A & Affin Ia = Affin A )
let I be affinely-independent Subset of V; ::_thesis: ( I c= A implies ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A ) )
assume A1: I c= A ; ::_thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
A2: A c= Affin A by Lm7;
percases ( I is empty or not I is empty ) ;
supposeA3: I is empty ; ::_thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
percases ( A is empty or not A is empty ) ;
supposeA4: A is empty ; ::_thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
take  I ; ::_thesis: ( I c= I & I c= A & Affin I = Affin A )
thus  ( I c= I & I c= A & Affin I = Affin A ) by A3, A4; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
then consider p being set  such that
A5: p in A by XBOOLE_0:def_1;
reconsider p = p as Element of V by A5;
set L = Lin ((- p) + A);
 (- p) + A c= [#] (Lin ((- p) + A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- p) + A or x in [#] (Lin ((- p) + A)) )
assume  x in (- p) + A ; ::_thesis: x in [#] (Lin ((- p) + A))
then  x in Lin ((- p) + A) by RLVECT_3:15;
hence  x in [#] (Lin ((- p) + A)) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider pA = (- p) + A as Subset of (Lin ((- p) + A)) ;
 Lin ((- p) + A) = Lin pA by RLVECT_5:20;
then consider Ia being Subset of (Lin ((- p) + A)) such that
A6: Ia c= pA and
A7: Ia is linearly-independent and
A8: Lin Ia = Lin ((- p) + A) by RLVECT_3:25;
 [#] (Lin ((- p) + A)) c= [#] V by RLSUB_1:def_2;
then reconsider IA = Ia as Subset of V by XBOOLE_1:1;
set IA0 = IA \/ {(0. V)};
 not 0. V in IA by A7, RLVECT_3:6, RLVECT_5:14;
then A9: (IA \/ {(0. V)}) \ {(0. V)} = IA by ZFMISC_1:117;
 0. V in {(0. V)} by TARSKI:def_1;
then A10: 0. V in IA \/ {(0. V)} by XBOOLE_0:def_3;
 IA is linearly-independent by A7, RLVECT_5:14;
then  IA \/ {(0. V)} is affinely-independent by A9, A10, Th46;
then reconsider pIA0 = p + (IA \/ {(0. V)}) as affinely-independent Subset of V ;
take  pIA0 ; ::_thesis: ( I c= pIA0 & pIA0 c= A & Affin pIA0 = Affin A )
thus  I c= pIA0 by A3, XBOOLE_1:2; ::_thesis: ( pIA0 c= A & Affin pIA0 = Affin A )
thus  pIA0 c= A ::_thesis: Affin pIA0 = Affin A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in pIA0 or x in A )
assume  x in pIA0 ; ::_thesis: x in A
then consider v being VECTOR of V such that
A11: x = p + v and
A12: v in IA \/ {(0. V)} ;
percases ( v in IA or v in {(0. V)} ) by A12, XBOOLE_0:def_3;
suppose v in IA ; ::_thesis: x in A
then  v in  {  ((- p) + w) where w is VECTOR of V : w in A  }  by A6;
then consider w being VECTOR of V such that
A13: v = (- p) + w and
A14: w in A ;
x = (p + (- p)) + w by A11, A13, RLVECT_1:def_3
.= (0. V) + w by RLVECT_1:5
.= w by RLVECT_1:4 ;
hence  x in A by A14; ::_thesis: verum
end;
suppose v in {(0. V)} ; ::_thesis: x in A
then  v = 0. V by TARSKI:def_1;
hence  x in A by A5, A11, RLVECT_1:4; ::_thesis: verum
end;
end;
end;
A15: pIA0 c= Affin pIA0 by Lm7;
A16: (- p) + pIA0 = ((- p) + p) + (IA \/ {(0. V)}) by Th5
.= (0. V) + (IA \/ {(0. V)}) by RLVECT_1:5
.= IA \/ {(0. V)} by Th6 ;
 p + (0. V) = p by RLVECT_1:def_4;
then  p in pIA0 by A10;
hence  Affin pIA0 = p + (Up (Lin (IA \/ {(0. V)}))) by A15, A16, Th57
.= p + (Up (Lin IA)) by Lm9
.= p + (Up (Lin ((- p) + A))) by A8, RLVECT_5:20
.= Affin A by A2, A5, Th57 ;
::_thesis: verum
end;
end;
end;
suppose not I is empty ; ::_thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
then consider p being set  such that
A17: p in I by XBOOLE_0:def_1;
reconsider p = p as Element of V by A17;
A18: ((- p) + I) \ {(0. V)} is linearly-independent by A17, Th41;
A19: (- p) + I c= (- p) + A by A1, RLTOPSP1:8;
set L = Lin ((- p) + A);
A20: ((- p) + I) \ {(0. V)} c= (- p) + I by XBOOLE_1:36;
A21: (- p) + A c= Up (Lin ((- p) + A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- p) + A or x in Up (Lin ((- p) + A)) )
assume  x in (- p) + A ; ::_thesis: x in Up (Lin ((- p) + A))
then  x in Lin ((- p) + A) by RLVECT_3:15;
hence  x in Up (Lin ((- p) + A)) by STRUCT_0:def_5; ::_thesis: verum
end;
then  (- p) + I c= Up (Lin ((- p) + A)) by A19, XBOOLE_1:1;
then reconsider pI0 = ((- p) + I) \ {(0. V)}, pA = (- p) + A as Subset of (Lin ((- p) + A)) by A20, A21, XBOOLE_1:1;
 ( Lin ((- p) + A) = Lin pA & pI0 c= pA ) by A19, A20, RLVECT_5:20, XBOOLE_1:1;
then consider i being linearly-independent Subset of (Lin ((- p) + A)) such that
A22: pI0 c= i and
A23: i c= pA and
A24: Lin i = Lin ((- p) + A) by A18, Th15, RLVECT_5:15;
reconsider Ia = i as linearly-independent Subset of V by RLVECT_5:14;
set I0 = Ia \/ {(0. V)};
A25: 0. V in {(0. V)} by TARSKI:def_1;
 not 0. V in Ia by RLVECT_3:6;
then  ( (Ia \/ {(0. V)}) \ {(0. V)} = Ia & 0. V in Ia \/ {(0. V)} ) by A25, XBOOLE_0:def_3, ZFMISC_1:117;
then  Ia \/ {(0. V)} is affinely-independent by Th46;
then reconsider pI0 = p + (Ia \/ {(0. V)}) as affinely-independent Subset of V ;
take  pI0 ; ::_thesis: ( I c= pI0 & pI0 c= A & Affin pI0 = Affin A )
A26: (- p) + p = 0. V by RLVECT_1:5;
then A27: p + ((- p) + I) = (0. V) + I by Th5
.= I by Th6 ;
 0. V in  {  ((- p) + v) where v is Element of V : v in I  }  by A17, A26;
then  (((- p) + I) \ {(0. V)}) \/ {(0. V)} = (- p) + I by ZFMISC_1:116;
then A28: (- p) + I c= Ia \/ {(0. V)} by A22, XBOOLE_1:9;
hence  I c= pI0 by A27, RLTOPSP1:8; ::_thesis: ( pI0 c= A & Affin pI0 = Affin A )
 p + ((- p) + I) c= pI0 by A28, RLTOPSP1:8;
then A29: p in pI0 by A17, A27;
thus  pI0 c= A ::_thesis: Affin pI0 = Affin A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in pI0 or x in A )
assume  x in pI0 ; ::_thesis: x in A
then consider v being VECTOR of V such that
A30: x = p + v and
A31: v in Ia \/ {(0. V)} ;
percases ( v in Ia or v in {(0. V)} ) by A31, XBOOLE_0:def_3;
suppose v in Ia ; ::_thesis: x in A
then  v in  {  ((- p) + w) where w is VECTOR of V : w in A  }  by A23;
then consider w being VECTOR of V such that
A32: v = (- p) + w and
A33: w in A ;
x = (p + (- p)) + w by A30, A32, RLVECT_1:def_3
.= (0. V) + w by RLVECT_1:5
.= w by RLVECT_1:4 ;
hence  x in A by A33; ::_thesis: verum
end;
suppose v in {(0. V)} ; ::_thesis: x in A
then  v = 0. V by TARSKI:def_1;
then  x = p by A30, RLVECT_1:4;
hence  x in A by A1, A17; ::_thesis: verum
end;
end;
end;
A34: pI0 c= Affin pI0 by Lm7;
A35: p in A by A1, A17;
(- p) + pI0 = (0. V) + (Ia \/ {(0. V)}) by A26, Th5
.= Ia \/ {(0. V)} by Th6 ;
hence  Affin pI0 = p + (Up (Lin (Ia \/ {(0. V)}))) by A29, A34, Th57
.= p + (Up (Lin Ia)) by Lm9
.= p + (Up (Lin ((- p) + A))) by A24, RLVECT_5:20
.= Affin A by A2, A35, Th57 ;
::_thesis: verum
end;
end;
end;

theorem :: RLAFFIN1:61
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent & Affin A = Affin B & card B <= card A holds
B is affinely-independent
proof
let V be RealLinearSpace; ::_thesis: for A, B being finite Subset of V st A is affinely-independent & Affin A = Affin B & card B <= card A holds
B is affinely-independent
let A, B be finite Subset of V; ::_thesis: ( A is affinely-independent & Affin A = Affin B & card B <= card A implies B is affinely-independent )
assume that
A1: A is affinely-independent and
A2: Affin A = Affin B and
A3: card B <= card A ; ::_thesis: B is affinely-independent
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: B is affinely-independent
then  B is empty by A3, XXREAL_0:1;
hence  B is affinely-independent ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: B is affinely-independent
then consider p being set  such that
A4: p in A by XBOOLE_0:def_1;
 card A > 0 by A4;
then reconsider n = (card A) - 1 as Element of NAT by NAT_1:20;
A5: A c= Affin A by Lm7;
reconsider p = p as Element of V by A4;
set L = Lin ((- p) + A);
 {} V c= B by XBOOLE_1:2;
then consider Ia being affinely-independent Subset of V such that
 {} V c= Ia and
A6: Ia c= B and
A7: Affin Ia = Affin B by Th60;
 not Ia is empty by A2, A4, A7;
then consider q being set  such that
A8: q in Ia by XBOOLE_0:def_1;
 (- p) + A c= [#] (Lin ((- p) + A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- p) + A or x in [#] (Lin ((- p) + A)) )
assume  x in (- p) + A ; ::_thesis: x in [#] (Lin ((- p) + A))
then  x in Lin ((- p) + A) by RLVECT_3:15;
hence  x in [#] (Lin ((- p) + A)) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider pA = (- p) + A as Subset of (Lin ((- p) + A)) ;
 ((- p) + A) \ {(0. V)} is linearly-independent by A1, A4, Th41;
then A9: pA \ {(0. V)} is linearly-independent by RLVECT_5:15;
 (- p) + p = 0. V by RLVECT_1:5;
then A10: 0. V in pA by A4;
then  Lin ((- p) + A) = Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116
.= Lin (((- p) + A) \ {(0. V)}) by Lm9
.= Lin (pA \ {(0. V)}) by RLVECT_5:20 ;
then A11: pA \ {(0. V)} is Basis of Lin ((- p) + A) by A9, RLVECT_3:def_3;
reconsider IA = Ia as finite set by A6;
A12: Ia c= Affin Ia by Lm7;
reconsider q = q as Element of V by A8;
p + (Lin ((- p) + A)) = p + (Up (Lin ((- p) + A))) by RUSUB_4:30
.= Affin A by A4, A5, Th57
.= q + (Up (Lin ((- q) + Ia))) by A2, A7, A8, A12, Th57
.= q + (Lin ((- q) + Ia)) by RUSUB_4:30 ;
then A13: Lin ((- p) + A) = Lin ((- q) + Ia) by RLSUB_1:69;
set qI = (- q) + Ia;
A14: (- q) + Ia c= [#] (Lin ((- q) + Ia))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- q) + Ia or x in [#] (Lin ((- q) + Ia)) )
assume  x in (- q) + Ia ; ::_thesis: x in [#] (Lin ((- q) + Ia))
then  x in Lin ((- q) + Ia) by RLVECT_3:15;
hence  x in [#] (Lin ((- q) + Ia)) by STRUCT_0:def_5; ::_thesis: verum
end;
 card pA = n + 1 by Th7;
then A15: card (pA \ {(0. V)}) = n by A10, STIRL2_1:55;
then  pA \ {(0. V)} is finite ;
then A16: Lin ((- p) + A) is finite-dimensional by A11, RLVECT_5:def_1;
reconsider qI = (- q) + Ia as Subset of (Lin ((- q) + Ia)) by A14;
 ((- q) + Ia) \ {(0. V)} is linearly-independent by A8, Th41;
then A17: qI \ {(0. V)} is linearly-independent by RLVECT_5:15;
 (- q) + q = 0. V by RLVECT_1:5;
then A18: 0. V in qI by A8;
then  Lin ((- q) + Ia) = Lin ((((- q) + Ia) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116
.= Lin (((- q) + Ia) \ {(0. V)}) by Lm9
.= Lin (qI \ {(0. V)}) by RLVECT_5:20 ;
then  qI \ {(0. V)} is Basis of Lin ((- q) + Ia) by A17, RLVECT_3:def_3;
then A19: card (qI \ {(0. V)}) = n by A11, A13, A15, A16, RLVECT_5:25;
then  ( not 0. V in qI \ {(0. V)} & qI \ {(0. V)} is finite ) by ZFMISC_1:56;
then A20: n + 1 = card ((qI \ {(0. V)}) \/ {(0. V)}) by A19, CARD_2:41
.= card qI by A18, ZFMISC_1:116
.= card Ia by Th7 ;
 card IA <= card B by A6, NAT_1:43;
hence  B is affinely-independent by A3, A6, A20, CARD_FIN:1, XXREAL_0:1; ::_thesis: verum
end;
end;
end;

theorem Th62: :: RLAFFIN1:62
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )
proof
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V holds
( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )
let L be Linear_Combination of V; ::_thesis: ( L is convex iff ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) ) )
hereby  ::_thesis: ( sum L = 1 & ( for v being VECTOR of V holds 0 <= L . v ) implies L is convex )
assume  L is convex ; ::_thesis: ( sum L = 1 & ( for v being Element of V holds L . b2 >= 0 ) )
then consider F being FinSequence of the carrier of V such that
A1: F is one-to-one and
A2: rng F = Carrier L and
A3: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by CONVEX1:def_3;
consider f being FinSequence of REAL  such that
A4: len f = len F and
A5: Sum f = 1 and
A6: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A3;
A7: len (L * F) = len F by FINSEQ_2:33;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_F_holds_
(L_*_F)_._k_=_f_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len F implies (L * F) . k = f . k )
assume A8: ( 1 <= k & k <= len F ) ; ::_thesis: (L * F) . k = f . k
then  k in dom f by A4, FINSEQ_3:25;
then A9: f . k = L . (F . k) by A6;
 k in dom (L * F) by A7, A8, FINSEQ_3:25;
hence  (L * F) . k = f . k by A9, FUNCT_1:12; ::_thesis: verum
end;
then  L * F = f by A4, A7, FINSEQ_1:14;
hence  sum L = 1 by A1, A2, A5, Def3; ::_thesis: for v being Element of V holds L . b2 >= 0
let v be Element of V; ::_thesis: L . b1 >= 0
percases ( v in Carrier L or not v in Carrier L ) ;
suppose v in Carrier L ; ::_thesis: L . b1 >= 0
then consider n being set  such that
A10: n in dom F and
A11: F . n = v by A2, FUNCT_1:def_3;
A12: dom f = dom F by A4, FINSEQ_3:29;
then  f . n = L . (F . n) by A6, A10;
hence  L . v >= 0 by A6, A10, A11, A12; ::_thesis: verum
end;
suppose not v in Carrier L ; ::_thesis: L . b1 >= 0
hence  L . v >= 0 ; ::_thesis: verum
end;
end;
end;
assume  sum L = 1 ; ::_thesis: ( ex v being VECTOR of V st not 0 <= L . v or L is convex )
then consider F being FinSequence of V such that
A13: ( F is one-to-one & rng F = Carrier L ) and
A14: 1 = Sum (L * F) by Def3;
assume A15: for v being Element of V holds L . v >= 0 ; ::_thesis: L is convex
now__::_thesis:_ex_F_being_FinSequence_of_V_st_
(_F_is_one-to-one_&_rng_F_=_Carrier_L_&_ex_f_being_FinSequence_of_REAL_st_
(_len_f_=_len_F_&_Sum_f_=_1_&_(_for_n_being_Nat_st_n_in_dom_f_holds_
(_f_._n_=_L_._(F_._n)_&_f_._n_>=_0_)_)_)_)
take F = F; ::_thesis: ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) )
thus  ( F is one-to-one & rng F = Carrier L ) by A13; ::_thesis: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) )
take f = L * F; ::_thesis: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) )
thus  ( len f = len F & Sum f = 1 ) by A14, FINSEQ_2:33; ::_thesis: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
then A16: dom F = dom f by FINSEQ_3:29;
let n be Nat; ::_thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A17: n in dom f ; ::_thesis: ( f . n = L . (F . n) & f . n >= 0 )
then A18: f . n = L . (F . n) by FUNCT_1:12;
 F . n = F /. n by A16, A17, PARTFUN1:def_6;
hence  ( f . n = L . (F . n) & f . n >= 0 ) by A15, A18; ::_thesis: verum
end;
hence  L is convex by CONVEX1:def_3; ::_thesis: verum
end;

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
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
L . x <= 1
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is convex holds
L . x <= 1
let L be Linear_Combination of V; ::_thesis: ( L is convex implies L . x <= 1 )
assume A1: L is convex ; ::_thesis: L . x <= 1
then  sum L = 1 by Th62;
then consider F being FinSequence of V such that
 F is one-to-one and
A2: rng F = Carrier L and
A3: 1 = Sum (L * F) by Def3;
assume A4: L . x > 1 ; ::_thesis: contradiction
then  x in dom L by FUNCT_1:def_2;
then reconsider v = x as Element of V by FUNCT_2:def_1;
 v in Carrier L by A4;
then consider n being set  such that
A5: n in dom F and
A6: F . n = v by A2, FUNCT_1:def_3;
 len (L * F) = len F by FINSEQ_2:33;
then A7: dom (L * F) = dom F by FINSEQ_3:29;
A8: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(L_*_F)_holds_
(L_*_F)_._i_>=_0
let i be Nat; ::_thesis: ( i in dom (L * F) implies (L * F) . i >= 0 )
assume  i in dom (L * F) ; ::_thesis: (L * F) . i >= 0
then  ( (L * F) . i = L . (F . i) & F . i = F /. i ) by A7, FUNCT_1:12, PARTFUN1:def_6;
hence  (L * F) . i >= 0 by A1, Th62; ::_thesis: verum
end;
reconsider n = n as Nat by A5;
 (L * F) . n = L . x by A5, A6, A7, FUNCT_1:12;
hence  contradiction by A3, A4, A5, A7, A8, MATRPROB:5; ::_thesis: verum
end;

theorem Th64: :: RLAFFIN1:64
for x being set
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex & L . x = 1 holds
Carrier L = {x}
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for L being Linear_Combination of V st L is convex & L . x = 1 holds
Carrier L = {x}
let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V st L is convex & L . x = 1 holds
Carrier L = {x}
let L be Linear_Combination of V; ::_thesis: ( L is convex & L . x = 1 implies Carrier L = {x} )
assume that
A1: L is convex and
A2: L . x = 1 ; ::_thesis: Carrier L = {x}
 x in dom L by A2, FUNCT_1:def_2;
then reconsider v = x as Element of V by FUNCT_2:def_1;
consider K being Linear_Combination of {v} such that
A3: K . v = 1 by RLVECT_4:37;
set LK = L - K;
A4: Carrier K c= {v} by RLVECT_2:def_6;
sum (L - K) = (sum L) - (sum K) by Th36
.= (sum L) - 1 by A3, A4, Th32
.= 1 - 1 by A1, Th62
.= 0 ;
then consider F being FinSequence of V such that
 F is one-to-one and
A5: rng F = Carrier (L - K) and
A6: 0 = Sum ((L - K) * F) by Def3;
 len ((L - K) * F) = len F by FINSEQ_2:33;
then A7: dom ((L - K) * F) = dom F by FINSEQ_3:29;
A8: for i being Nat st i in dom ((L - K) * F) holds
0 <= ((L - K) * F) . i
proof
let i be Nat; ::_thesis: ( i in dom ((L - K) * F) implies 0 <= ((L - K) * F) . i )
assume A9: i in dom ((L - K) * F) ; ::_thesis: 0 <= ((L - K) * F) . i
then A10: ((L - K) * F) . i = (L - K) . (F . i) by FUNCT_1:12;
A11: F . i in Carrier (L - K) by A5, A7, A9, FUNCT_1:def_3;
then A12: (L - K) . (F . i) = (L . (F . i)) - (K . (F . i)) by RLVECT_2:54;
percases ( F . i = v or F . i <> v ) ;
suppose F . i = v ; ::_thesis: 0 <= ((L - K) * F) . i
hence  0 <= ((L - K) * F) . i by A2, A3, A9, A12, FUNCT_1:12; ::_thesis: verum
end;
suppose F . i <> v ; ::_thesis: 0 <= ((L - K) * F) . i
then  not F . i in Carrier K by A4, TARSKI:def_1;
then  K . (F . i) = 0 by A11;
hence  0 <= ((L - K) * F) . i by A1, A10, A11, A12, Th62; ::_thesis: verum
end;
end;
end;
 Carrier (L - K) = {}
proof
assume  Carrier (L - K) <> {} ; ::_thesis: contradiction
then consider p being set  such that
A13: p in Carrier (L - K) by XBOOLE_0:def_1;
reconsider p = p as Element of V by A13;
consider i being set  such that
A14: i in dom F and
A15: F . i = p by A5, A13, FUNCT_1:def_3;
reconsider i = i as Nat by A14;
 ((L - K) * F) . i > 0
proof
A16: (L - K) . p = (L . p) - (K . p) by RLVECT_2:54;
percases ( p = v or p <> v ) ;
suppose p = v ; ::_thesis: ((L - K) * F) . i > 0
then  (L - K) . p = 1 - 1 by A2, A3, RLVECT_2:54;
hence  ((L - K) * F) . i > 0 by A13, RLVECT_2:19; ::_thesis: verum
end;
suppose p <> v ; ::_thesis: ((L - K) * F) . i > 0
then  not p in Carrier K by A4, TARSKI:def_1;
then  K . p = 0 ;
then A17: (L - K) . p >= 0 by A1, A16, Th62;
 (L - K) . p <> 0 by A13, RLVECT_2:19;
hence  ((L - K) * F) . i > 0 by A7, A14, A15, A17, FUNCT_1:12; ::_thesis: verum
end;
end;
end;
hence  contradiction by A6, A7, A8, A14, RVSUM_1:85; ::_thesis: verum
end;
then  ZeroLC V = L + (- K) by RLVECT_2:def_5;
then A18: - K = - L by RLVECT_2:50;
A19: v in Carrier L by A2;
 - (- L) = L by RLVECT_2:53;
then  K = L by A18, RLVECT_2:53;
hence  Carrier L = {x} by A4, A19, ZFMISC_1:33; ::_thesis: verum
end;

theorem Th65: :: RLAFFIN1:65
for V being RealLinearSpace
for A being Subset of V holds conv A c= Affin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds conv A c= Affin A
let A be Subset of V; ::_thesis: conv A c= Affin A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in conv A or x in Affin A )
assume A1: x in conv A ; ::_thesis: x in Affin A
then reconsider A1 = A as non empty Subset of V ;
 conv A1 =  {  (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V  }  by CONVEX3:5;
then consider L being Convex_Combination of A1 such that
A2: Sum L = x and
 L in ConvexComb V by A1;
 sum L = 1 by Th62;
then  x in  {  (Sum K) where K is Linear_Combination of A : sum K = 1  }  by A2;
hence  x in Affin A by Th59; ::_thesis: verum
end;

theorem :: RLAFFIN1:66
for x being set
for V being RealLinearSpace
for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds
x in A
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds
x in A
let V be RealLinearSpace; ::_thesis: for A being Subset of V st x in conv A & (conv A) \ {x} is convex holds
x in A
let A be Subset of V; ::_thesis: ( x in conv A & (conv A) \ {x} is convex implies x in A )
assume that
A1: x in conv A and
A2: (conv A) \ {x} is convex ; ::_thesis: x in A
reconsider A1 = A as non empty Subset of V by A1;
A3: conv A1 =  {  (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V  }  by CONVEX3:5;
assume A4: not x in A ; ::_thesis: contradiction
consider L being Convex_Combination of A1 such that
A5: Sum L = x and
 L in ConvexComb V by A1, A3;
set C = Carrier L;
A6: Carrier L c= A1 by RLVECT_2:def_6;
 Carrier L <> {} by CONVEX1:21;
then consider p being set  such that
A7: p in Carrier L by XBOOLE_0:def_1;
reconsider p = p as Element of V by A7;
A8: sum L = 1 by Th62;
 (Carrier L) \ {p} <> {}
proof
assume A9: (Carrier L) \ {p} = {} ; ::_thesis: contradiction
then  Carrier L = {p} by A7, ZFMISC_1:58;
then A10: L . p = 1 by A8, Th32;
 Sum L = (L . p) * p by A7, A9, RLVECT_2:35, ZFMISC_1:58;
then  x = p by A5, A10, RLVECT_1:def_8;
hence  contradiction by A4, A6, A7; ::_thesis: verum
end;
then consider q being set  such that
A11: q in (Carrier L) \ {p} by XBOOLE_0:def_1;
reconsider q = q as Element of V by A11;
A12: q in Carrier L by A11, XBOOLE_0:def_5;
then  L . q <> 0 by RLVECT_2:19;
then A13: L . q > 0 by Th62;
reconsider mm = min ((L . p),(L . q)) as Real by XREAL_0:def_1;
consider Lq being Linear_Combination of {q} such that
A14: Lq . q = mm by RLVECT_4:37;
A15: p <> q by A11, ZFMISC_1:56;
then A16: p - q <> 0. V by RLVECT_1:21;
A17: Carrier Lq c= {q} by RLVECT_2:def_6;
 {q} c= A by A6, A12, ZFMISC_1:31;
then  Carrier Lq c= A by A17, XBOOLE_1:1;
then A18: Lq is Linear_Combination of A by RLVECT_2:def_6;
consider Lp being Linear_Combination of {p} such that
A19: Lp . p = mm by RLVECT_4:37;
A20: Carrier Lp c= {p} by RLVECT_2:def_6;
 {p} c= A by A6, A7, ZFMISC_1:31;
then  Carrier Lp c= A by A20, XBOOLE_1:1;
then  Lp is Linear_Combination of A by RLVECT_2:def_6;
then A21: Lp - Lq is Linear_Combination of A by A18, RLVECT_2:56;
then  - (Lp - Lq) is Linear_Combination of A by RLVECT_2:52;
then reconsider Lpq = L + (Lp - Lq), L1pq = L - (Lp - Lq) as Linear_Combination of A1 by A21, RLVECT_2:38;
A22: Sum L1pq = (Sum L) - (Sum (Lp - Lq)) by RLVECT_3:4
.= (Sum L) + (- (Sum (Lp - Lq))) by RLVECT_1:def_11 ;
 L . p <> 0 by A7, RLVECT_2:19;
then  L . p > 0 by Th62;
then A23: mm > 0 by A13, XXREAL_0:15;
A24: for v being VECTOR of V holds L1pq . v >= 0
proof
let v be VECTOR of V; ::_thesis: L1pq . v >= 0
A25: L1pq . v = (L . v) - ((Lp - Lq) . v) by RLVECT_2:54
.= (L . v) - ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;
A26: L . v >= 0 by Th62;
percases ( v = q or v = p or ( v <> p & v <> q ) ) ;
supposeA27: v = q ; ::_thesis: L1pq . v >= 0
then  not v in Carrier Lp by A15, A20, TARSKI:def_1;
then  Lp . v = 0 ;
hence  L1pq . v >= 0 by A23, A14, A25, A26, A27; ::_thesis: verum
end;
supposeA28: v = p ; ::_thesis: L1pq . v >= 0
 L . p >= mm by XXREAL_0:17;
then A29: (L . p) - mm >= mm - mm by XREAL_1:9;
 not v in Carrier Lq by A15, A17, A28, TARSKI:def_1;
then  Lq . v = 0 ;
hence  L1pq . v >= 0 by A19, A25, A28, A29; ::_thesis: verum
end;
supposeA30: ( v <> p & v <> q ) ; ::_thesis: L1pq . v >= 0
then  not v in Carrier Lq by A17, TARSKI:def_1;
then A31: Lq . v = 0 ;
 not v in Carrier Lp by A20, A30, TARSKI:def_1;
then  Lp . v = 0 ;
hence  L1pq . v >= 0 by A25, A31, Th62; ::_thesis: verum
end;
end;
end;
Sum (Lp - Lq) = (Sum Lp) - (Sum Lq) by RLVECT_3:4
.= (mm * p) - (Sum Lq) by A19, RLVECT_2:32
.= (mm * p) - (mm * q) by A14, RLVECT_2:32
.= mm * (p - q) by RLVECT_1:34 ;
then A32: Sum (Lp - Lq) <> 0. V by A23, A16, RLVECT_1:11;
A33: sum (Lp - Lq) = (sum Lp) - (sum Lq) by Th36
.= mm - (sum Lq) by A19, A20, Th32
.= mm - mm by A14, A17, Th32
.= 0 ;
A34: for v being VECTOR of V holds Lpq . v >= 0
proof
let v be VECTOR of V; ::_thesis: Lpq . v >= 0
A35: Lpq . v = (L . v) + ((Lp - Lq) . v) by RLVECT_2:def_10
.= (L . v) + ((Lp . v) - (Lq . v)) by RLVECT_2:54 ;
A36: L . v >= 0 by Th62;
percases ( v = p or v = q or ( v <> p & v <> q ) ) ;
supposeA37: v = p ; ::_thesis: Lpq . v >= 0
then  not v in Carrier Lq by A15, A17, TARSKI:def_1;
then  Lpq . v = (L . v) + (mm - 0) by A19, A35, A37;
hence  Lpq . v >= 0 by A23, A36; ::_thesis: verum
end;
supposeA38: v = q ; ::_thesis: Lpq . v >= 0
 L . q >= mm by XXREAL_0:17;
then A39: (L . q) - mm >= mm - mm by XREAL_1:9;
 not v in Carrier Lp by A15, A20, A38, TARSKI:def_1;
then  Lp . v = 0 ;
hence  Lpq . v >= 0 by A14, A35, A38, A39; ::_thesis: verum
end;
supposeA40: ( v <> p & v <> q ) ; ::_thesis: Lpq . v >= 0
then  not v in Carrier Lq by A17, TARSKI:def_1;
then A41: Lq . v = 0 ;
 not v in Carrier Lp by A20, A40, TARSKI:def_1;
then  Lp . v = 0 ;
hence  Lpq . v >= 0 by A35, A41, Th62; ::_thesis: verum
end;
end;
end;
sum L1pq = (sum L) - (sum (Lp - Lq)) by Th36
.= 1 + 0 by A33, Th62 ;
then A42: L1pq is convex by A24, Th62;
then  L1pq in ConvexComb V by CONVEX3:def_1;
then A43: Sum L1pq in conv A1 by A3, A42;
sum Lpq = (sum L) + (sum (Lp - Lq)) by Th34
.= 1 + 0 by A33, Th62 ;
then A44: Lpq is convex by A34, Th62;
then  Lpq in ConvexComb V by CONVEX3:def_1;
then A45: Sum Lpq in conv A by A3, A44;
 0. V = - (0. V) by RLVECT_1:12;
then  - (Sum (Lp - Lq)) <> 0. V by A32, RLVECT_1:18;
then  Sum L1pq <> x by A5, A22, RLVECT_1:9;
then A46: Sum L1pq in (conv A) \ {x} by A43, ZFMISC_1:56;
 Sum Lpq = (Sum L) + (Sum (Lp - Lq)) by RLVECT_3:1;
then  Sum Lpq <> x by A5, A32, RLVECT_1:9;
then A47: Sum Lpq in (conv A) \ {x} by A45, ZFMISC_1:56;
((1 / 2) * (Sum Lpq)) + ((1 - (1 / 2)) * (Sum L1pq)) = ((1 / 2) * ((Sum L) + (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by A22, RLVECT_3:1
.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + ((1 / 2) * ((Sum L) + (- (Sum (Lp - Lq))))) by RLVECT_1:def_5
.= (((1 / 2) * (Sum L)) + ((1 / 2) * (Sum (Lp - Lq)))) + (((1 / 2) * (Sum L)) + ((1 / 2) * (- (Sum (Lp - Lq))))) by RLVECT_1:def_5
.= ((1 / 2) * (Sum L)) + (((1 / 2) * (Sum (Lp - Lq))) + (((1 / 2) * (- (Sum (Lp - Lq)))) + ((1 / 2) * (Sum L)))) by RLVECT_1:def_3
.= ((1 / 2) * (Sum L)) + ((((1 / 2) * (Sum (Lp - Lq))) + ((1 / 2) * (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def_3
.= ((1 / 2) * (Sum L)) + (((1 / 2) * ((Sum (Lp - Lq)) + (- (Sum (Lp - Lq))))) + ((1 / 2) * (Sum L))) by RLVECT_1:def_5
.= ((1 / 2) * (Sum L)) + (((1 / 2) * (0. V)) + ((1 / 2) * (Sum L))) by RLVECT_1:5
.= ((1 / 2) * (Sum L)) + ((0. V) + ((1 / 2) * (Sum L))) by RLVECT_1:10
.= ((1 / 2) * (Sum L)) + ((1 / 2) * (Sum L)) by RLVECT_1:def_4
.= ((1 / 2) + (1 / 2)) * (Sum L) by RLVECT_1:def_6
.= Sum L by RLVECT_1:def_8 ;
then  Sum L in (conv A) \ {x} by A2, A46, A47, CONVEX1:def_2;
hence  contradiction by A5, ZFMISC_1:56; ::_thesis: verum
end;

theorem Th67: :: RLAFFIN1:67
for V being RealLinearSpace
for A being Subset of V holds Affin (conv A) = Affin A
proof
let V be RealLinearSpace; ::_thesis: for A being Subset of V holds Affin (conv A) = Affin A
let A be Subset of V; ::_thesis: Affin (conv A) = Affin A
thus  Affin (conv A) c= Affin A by Th51, Th65; :: according to XBOOLE_0:def_10 ::_thesis: Affin A c= Affin (conv A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Affin A or x in Affin (conv A) )
assume  x in Affin A ; ::_thesis: x in Affin (conv A)
then  x in  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  by Th59;
then consider L being Linear_Combination of A such that
A1: x = Sum L and
A2: sum L = 1 ;
reconsider K = L as Linear_Combination of conv A by Lm1, RLVECT_2:21;
 Sum K in  {  (Sum M) where M is Linear_Combination of conv A : sum M = 1  }  by A2;
hence  x in Affin (conv A) by A1, Th59; ::_thesis: verum
end;

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
proof
let V be RealLinearSpace; ::_thesis: for A, B being Subset of V st conv A c= conv B holds
Affin A c= Affin B
let A, B be Subset of V; ::_thesis: ( conv A c= conv B implies Affin A c= Affin B )
 ( Affin (conv A) = Affin A & Affin (conv B) = Affin B ) by Th67;
hence  ( conv A c= conv B implies Affin A c= Affin B ) by Th52; ::_thesis: verum
end;

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
proof
let RLS be non empty RLSStruct ; ::_thesis: for A, B being Subset of RLS st A c= Affin B holds
Affin (A \/ B) = Affin B
let A, B be Subset of RLS; ::_thesis: ( A c= Affin B implies Affin (A \/ B) = Affin B )
assume A1: A c= Affin B ; ::_thesis: Affin (A \/ B) = Affin B
set AB =  {  C where C is Affine Subset of RLS : A \/ B c= C  }  ;
 B c= Affin B by Lm7;
then  A \/ B c= Affin B by A1, XBOOLE_1:8;
then  Affin B in  {  C where C is Affine Subset of RLS : A \/ B c= C  }  ;
then A2: Affin (A \/ B) c= Affin B by SETFAM_1:3;
 Affin B c= Affin (A \/ B) by Th52, XBOOLE_1:7;
hence  Affin (A \/ B) = Affin B by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

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 & sum it = 1 );
existence
 ex b1 being Linear_Combination of A st
( Sum b1 = x & sum b1 = 1 )
proof
 Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  by Th59;
hence  ex b1 being Linear_Combination of A st
( Sum b1 = x & sum b1 = 1 ) by B2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Linear_Combination of A st Sum b1 = x & sum b1 = 1 & Sum b2 = x & sum b2 = 1 holds
b1 = b2
proof
let L1, L2 be Linear_Combination of A; ::_thesis: ( Sum L1 = x & sum L1 = 1 & Sum L2 = x & sum L2 = 1 implies L1 = L2 )
assume that
A1: Sum L1 = x and
A2: sum L1 = 1 and
A3: Sum L2 = x and
A4: sum L2 = 1 ; ::_thesis: L1 = L2
A5: Sum (L1 - L2) = (Sum L1) - (Sum L1) by A1, A3, RLVECT_3:4
.= 0. V by RLVECT_1:15 ;
A6: L1 - L2 is Linear_Combination of A by RLVECT_2:56;
sum (L1 - L2) = 1 - 1 by A2, A4, Th36
.= 0 ;
then  Carrier (L1 - L2) = {} by B1, A5, A6, Th42;
then  ZeroLC V = L1 + (- L2) by RLVECT_2:def_5;
then A7: - L2 = - L1 by RLVECT_2:50;
 L1 = - (- L1) by RLVECT_2:53;
hence  L1 = L2 by A7, RLVECT_2:53; ::_thesis: verum
end;
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 & 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 & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for v1, v2 being VECTOR of V
for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
let v1, v2 be VECTOR of V; ::_thesis: for I being affinely-independent Subset of V st v1 in Affin I & v2 in Affin I holds
(((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
let I be affinely-independent Subset of V; ::_thesis: ( v1 in Affin I & v2 in Affin I implies (((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)) )
assume that
A1: v1 in Affin I and
A2: v2 in Affin I ; ::_thesis: (((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))
set rv12 = ((1 - r) * v1) + (r * v2);
A3: ((1 - r) * v1) + (r * v2) in Affin I by A1, A2, RUSUB_4:def_4;
 ( (1 - r) * (v1 |-- I) is Linear_Combination of I & r * (v2 |-- I) is Linear_Combination of I ) by RLVECT_2:44;
then A4: ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)) is Linear_Combination of I by RLVECT_2:38;
A5: Sum (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))) = (Sum ((1 - r) * (v1 |-- I))) + (Sum (r * (v2 |-- I))) by RLVECT_3:1
.= ((1 - r) * (Sum (v1 |-- I))) + (Sum (r * (v2 |-- I))) by RLVECT_3:2
.= ((1 - r) * (Sum (v1 |-- I))) + (r * (Sum (v2 |-- I))) by RLVECT_3:2
.= ((1 - r) * v1) + (r * (Sum (v2 |-- I))) by A1, Def7
.= ((1 - r) * v1) + (r * v2) by A2, Def7 ;
sum (((1 - r) * (v1 |-- I)) + (r * (v2 |-- I))) = (sum ((1 - r) * (v1 |-- I))) + (sum (r * (v2 |-- I))) by Th34
.= ((1 - r) * (sum (v1 |-- I))) + (sum (r * (v2 |-- I))) by Th35
.= ((1 - r) * (sum (v1 |-- I))) + (r * (sum (v2 |-- I))) by Th35
.= ((1 - r) * 1) + (r * (sum (v2 |-- I))) by A1, Def7
.= ((1 - r) * 1) + (r * 1) by A2, Def7
.= 1 ;
hence  (((1 - r) * v1) + (r * v2)) |-- I = ((1 - r) * (v1 |-- I)) + (r * (v2 |-- I)) by A3, A4, A5, Def7; ::_thesis: verum
end;

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 & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
proof
let x be set ; ::_thesis: 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 & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
let v be VECTOR of V; ::_thesis: for I being affinely-independent Subset of V st x in conv I holds
( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
let I be affinely-independent Subset of V; ::_thesis: ( x in conv I implies ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) )
assume A1: x in conv I ; ::_thesis: ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 )
then reconsider I1 = I as non empty Subset of V ;
 conv I1 =  {  (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V  }  by CONVEX3:5;
then consider L being Convex_Combination of I1 such that
A2: Sum L = x and
 L in ConvexComb V by A1;
 ( conv I c= Affin I & sum L = 1 ) by Th62, Th65;
then  L = x |-- I by A1, A2, Def7;
hence  ( x |-- I is convex & 0 <= (x |-- I) . v & (x |-- I) . v <= 1 ) by Th62, Th63; ::_thesis: verum
end;

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 & x in I ) )
proof
let x, y be set ; ::_thesis: 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 & x in I ) )
let V be RealLinearSpace; ::_thesis: for I being affinely-independent Subset of V st x in conv I holds
( (x |-- I) . y = 1 iff ( x = y & x in I ) )
let I be affinely-independent Subset of V; ::_thesis: ( x in conv I implies ( (x |-- I) . y = 1 iff ( x = y & x in I ) ) )
assume A1: x in conv I ; ::_thesis: ( (x |-- I) . y = 1 iff ( x = y & x in I ) )
then reconsider v = x as Element of V ;
hereby  ::_thesis: ( x = y & x in I implies (x |-- I) . y = 1 )
assume A2: (x |-- I) . y = 1 ; ::_thesis: ( x = y & x in I )
 x |-- I is convex by A1, Th71;
then A3: Carrier (x |-- I) = {y} by A2, Th64;
 y in {y} by TARSKI:def_1;
then reconsider v = y as Element of V by A3;
 conv I c= Affin I by Th65;
hence A4: x = Sum (x |-- I) by A1, Def7
.= ((x |-- I) . v) * v by A3, RLVECT_2:35
.= y by A2, RLVECT_1:def_8 ;
::_thesis: x in I
 ( Carrier (x |-- I) c= I & v in Carrier (x |-- I) ) by A2, RLVECT_2:def_6;
hence  x in I by A4; ::_thesis: verum
end;
assume that
A5: x = y and
A6: x in I ; ::_thesis: (x |-- I) . y = 1
consider L being Linear_Combination of {v} such that
A7: L . v = 1 by RLVECT_4:37;
 Carrier L c= {v} by RLVECT_2:def_6;
then A8: sum L = 1 by A7, Th32;
A9: I c= Affin I by Lm7;
 {v} c= I by A6, ZFMISC_1:31;
then A10: L is Linear_Combination of I by RLVECT_2:21;
Sum L = 1 * v by A7, RLVECT_2:32
.= v by RLVECT_1:def_8 ;
hence  (x |-- I) . y = 1 by A5, A6, A7, A8, A9, A10, Def7; ::_thesis: verum
end;

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 & ( for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ) holds
x in conv I
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ) holds
x in conv I
let V be RealLinearSpace; ::_thesis: for I being affinely-independent Subset of V st x in Affin I & ( for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ) holds
x in conv I
let I be affinely-independent Subset of V; ::_thesis: ( x in Affin I & ( for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ) implies x in conv I )
assume that
A1: x in Affin I and
A2: for v being VECTOR of V st v in I holds
0 <= (x |-- I) . v ; ::_thesis: x in conv I
set xI = x |-- I;
A3: Sum (x |-- I) = x by A1, Def7;
reconsider I1 = I as non empty Subset of V by A1;
A4: for v being VECTOR of V holds 0 <= (x |-- I) . v
proof
let v be VECTOR of V; ::_thesis: 0 <= (x |-- I) . v
A5: ( v in Carrier (x |-- I) or not v in Carrier (x |-- I) ) ;
 Carrier (x |-- I) c= I by RLVECT_2:def_6;
hence  0 <= (x |-- I) . v by A2, A5; ::_thesis: verum
end;
 sum (x |-- I) = 1 by A1, Def7;
then A6: x |-- I is convex by A4, Th62;
then  ( conv I1 =  {  (Sum L) where L is Convex_Combination of I1 : L in ConvexComb V  }  & x |-- I in ConvexComb V ) by CONVEX3:5, CONVEX3:def_1;
hence  x in conv I by A3, A6; ::_thesis: verum
end;

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
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V st x in I holds
(conv I) \ {x} is convex
let V be RealLinearSpace; ::_thesis: for I being affinely-independent Subset of V st x in I holds
(conv I) \ {x} is convex
let I be affinely-independent Subset of V; ::_thesis: ( x in I implies (conv I) \ {x} is convex )
assume A1: x in I ; ::_thesis: (conv I) \ {x} is convex
then reconsider X = x as Element of V ;
A2: conv I c= Affin I by Th65;
now__::_thesis:_for_v1,_v2_being_VECTOR_of_V
for_r_being_Real_st_0_<_r_&_r_<_1_&_v1_in_(conv_I)_\_{x}_&_v2_in_(conv_I)_\_{x}_holds_
(r_*_v1)_+_((1_-_r)_*_v2)_in_(conv_I)_\_{x}
let v1, v2 be VECTOR of V; ::_thesis: for r being Real st 0 < r & r < 1 & v1 in (conv I) \ {x} & v2 in (conv I) \ {x} holds
(r * v1) + ((1 - r) * v2) in (conv I) \ {x}
let r be Real; ::_thesis: ( 0 < r & r < 1 & v1 in (conv I) \ {x} & v2 in (conv I) \ {x} implies (r * v1) + ((1 - r) * v2) in (conv I) \ {x} )
set rv12 = (r * v1) + ((1 - r) * v2);
assume that
A3: 0 < r and
A4: r < 1 ; ::_thesis: ( v1 in (conv I) \ {x} & v2 in (conv I) \ {x} implies (r * v1) + ((1 - r) * v2) in (conv I) \ {x} )
assume that
A5: v1 in (conv I) \ {x} and
A6: v2 in (conv I) \ {x} ; ::_thesis: (r * v1) + ((1 - r) * v2) in (conv I) \ {x}
A7: 1 - r > 1 - 1 by A4, XREAL_1:10;
A8: v2 in conv I by A6, ZFMISC_1:56;
then A9: (v2 |-- I) . X <= 1 by Th71;
A10: v1 in conv I by A5, ZFMISC_1:56;
then A11: (v1 |-- I) . X <= 1 by Th71;
A12: ((r * v1) + ((1 - r) * v2)) |-- I = ((1 - r) * (v2 |-- I)) + (r * (v1 |-- I)) by A2, A10, A8, Th70;
A13: now__::_thesis:_for_w_being_VECTOR_of_V_st_w_in_I_holds_
0_<=_(((r_*_v1)_+_((1_-_r)_*_v2))_|--_I)_._w
let w be VECTOR of V; ::_thesis: ( w in I implies 0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w )
assume  w in I ; ::_thesis: 0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w
A14: (((r * v1) + ((1 - r) * v2)) |-- I) . w = (((1 - r) * (v2 |-- I)) . w) + ((r * (v1 |-- I)) . w) by A12, RLVECT_2:def_10
.= ((1 - r) * ((v2 |-- I) . w)) + ((r * (v1 |-- I)) . w) by RLVECT_2:def_11
.= ((1 - r) * ((v2 |-- I) . w)) + (r * ((v1 |-- I) . w)) by RLVECT_2:def_11 ;
 ( (v2 |-- I) . w >= 0 & (v1 |-- I) . w >= 0 ) by A10, A8, Th71;
hence  0 <= (((r * v1) + ((1 - r) * v2)) |-- I) . w by A3, A7, A14; ::_thesis: verum
end;
 (r * v1) + ((1 - r) * v2) in Affin I by A2, A10, A8, RUSUB_4:def_4;
then A15: (r * v1) + ((1 - r) * v2) in conv I by A13, Th73;
 v1 <> x by A5, ZFMISC_1:56;
then  (v1 |-- I) . X <> 1 by A10, Th72;
then  (v1 |-- I) . X < 1 by A11, XXREAL_0:1;
then A16: r * ((v1 |-- I) . X) < r * 1 by A3, XREAL_1:68;
 v2 <> x by A6, ZFMISC_1:56;
then  (v2 |-- I) . X <> 1 by A8, Th72;
then  (v2 |-- I) . X < 1 by A9, XXREAL_0:1;
then  (1 - r) * ((v2 |-- I) . X) < (1 - r) * 1 by A7, XREAL_1:68;
then A17: ((1 - r) * ((v2 |-- I) . X)) + (r * ((v1 |-- I) . X)) < ((1 - r) * 1) + (r * 1) by A16, XREAL_1:8;
(((r * v1) + ((1 - r) * v2)) |-- I) . X = (((1 - r) * (v2 |-- I)) . X) + ((r * (v1 |-- I)) . X) by A12, RLVECT_2:def_10
.= ((1 - r) * ((v2 |-- I) . X)) + ((r * (v1 |-- I)) . X) by RLVECT_2:def_11
.= ((1 - r) * ((v2 |-- I) . X)) + (r * ((v1 |-- I) . X)) by RLVECT_2:def_11 ;
then  (r * v1) + ((1 - r) * v2) <> X by A1, A15, A17, Th72;
hence  (r * v1) + ((1 - r) * v2) in (conv I) \ {x} by A15, ZFMISC_1:56; ::_thesis: verum
end;
hence  (conv I) \ {x} is convex by CONVEX1:def_2; ::_thesis: verum
end;

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 & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
let V be RealLinearSpace; ::_thesis: for I being affinely-independent Subset of V
for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
let I be affinely-independent Subset of V; ::_thesis: for B being Subset of V st x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
let B be Subset of V; ::_thesis: ( x in Affin I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) implies ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) )
assume that
A1: x in Affin I and
A2: for y being set st y in B holds
(x |-- I) . y = 0 ; ::_thesis: ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) )
A3: Affin I =  {  (Sum L) where L is Linear_Combination of I : sum L = 1  }  by Th59;
A4: I \ B is affinely-independent by Th43, XBOOLE_1:36;
consider L being Linear_Combination of I such that
A5: ( x = Sum L & sum L = 1 ) by A1, A3;
A6: x |-- I = L by A1, A5, Def7;
 Carrier L c= I \ B
proof
A7: Carrier L c= I by RLVECT_2:def_6;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Carrier L or y in I \ B )
assume A8: y in Carrier L ; ::_thesis: y in I \ B
assume  not y in I \ B ; ::_thesis: contradiction
then  y in B by A7, A8, XBOOLE_0:def_5;
then  L . y = 0 by A2, A6;
hence  contradiction by A8, RLVECT_2:19; ::_thesis: verum
end;
then A9: L is Linear_Combination of I \ B by RLVECT_2:def_6;
then  x in  {  (Sum K) where K is Linear_Combination of I \ B : sum K = 1  }  by A5;
then  x in Affin (I \ B) by Th59;
hence  ( x in Affin (I \ B) & x |-- I = x |-- (I \ B) ) by A4, A5, A6, A9, Def7; ::_thesis: verum
end;

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 & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for I being affinely-independent Subset of V
for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
let V be RealLinearSpace; ::_thesis: for I being affinely-independent Subset of V
for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
let I be affinely-independent Subset of V; ::_thesis: for B being Subset of V st x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) holds
x in conv (I \ B)
let B be Subset of V; ::_thesis: ( x in conv I & ( for y being set st y in B holds
(x |-- I) . y = 0 ) implies x in conv (I \ B) )
assume that
A1: x in conv I and
A2: for y being set st y in B holds
(x |-- I) . y = 0 ; ::_thesis: x in conv (I \ B)
set IB = I \ B;
A3: conv I c= Affin I by Th65;
then  x |-- I = x |-- (I \ B) by A1, A2, Th75;
then A4: for v being VECTOR of V st v in I \ B holds
0 <= (x |-- (I \ B)) . v by A1, Th71;
A5: I \ B is affinely-independent by Th43, XBOOLE_1:36;
 x in Affin (I \ B) by A1, A2, A3, Th75;
hence  x in conv (I \ B) by A4, A5, Th73; ::_thesis: verum
end;

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 & x in Affin B holds
x |-- B = x |-- I
proof
let x be set ; ::_thesis: for V being RealLinearSpace
for B being Subset of V
for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
let V be RealLinearSpace; ::_thesis: for B being Subset of V
for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
let B be Subset of V; ::_thesis: for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
let I be affinely-independent Subset of V; ::_thesis: ( B c= I & x in Affin B implies x |-- B = x |-- I )
assume that
A1: B c= I and
A2: x in Affin B ; ::_thesis: x |-- B = x |-- I
 B is affinely-independent by A1, Th43;
then A3: ( Sum (x |-- B) = x & sum (x |-- B) = 1 ) by A2, Def7;
 ( Affin B c= Affin I & x |-- B is Linear_Combination of I ) by A1, Th52, RLVECT_2:21;
hence  x |-- B = x |-- I by A2, A3, Def7; ::_thesis: verum
end;

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 & v2 in Affin A & r + s = 1 holds
(r * v1) + (s * v2) in Affin A
proof
let r, s be Real; ::_thesis: for V being RealLinearSpace
for v1, v2 being VECTOR of V
for A being Subset of V st v1 in Affin A & v2 in Affin A & r + s = 1 holds
(r * v1) + (s * v2) in Affin A
let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V
for A being Subset of V st v1 in Affin A & v2 in Affin A & r + s = 1 holds
(r * v1) + (s * v2) in Affin A
let v1, v2 be VECTOR of V; ::_thesis: for A being Subset of V st v1 in Affin A & v2 in Affin A & r + s = 1 holds
(r * v1) + (s * v2) in Affin A
let A be Subset of V; ::_thesis: ( v1 in Affin A & v2 in Affin A & r + s = 1 implies (r * v1) + (s * v2) in Affin A )
A1: Affin A =  {  (Sum L) where L is Linear_Combination of A : sum L = 1  }  by Th59;
assume  v1 in Affin A ; ::_thesis: ( not v2 in Affin A or not r + s = 1 or (r * v1) + (s * v2) in Affin A )
then consider L1 being Linear_Combination of A such that
A2: v1 = Sum L1 and
A3: sum L1 = 1 by A1;
assume  v2 in Affin A ; ::_thesis: ( not r + s = 1 or (r * v1) + (s * v2) in Affin A )
then consider L2 being Linear_Combination of A such that
A4: v2 = Sum L2 and
A5: sum L2 = 1 by A1;
A6: Sum ((r * L1) + (s * L2)) = (Sum (r * L1)) + (Sum (s * L2)) by RLVECT_3:1
.= (r * (Sum L1)) + (Sum (s * L2)) by RLVECT_3:2
.= (r * v1) + (s * v2) by A2, A4, RLVECT_3:2 ;
 ( r * L1 is Linear_Combination of A & s * L2 is Linear_Combination of A ) by RLVECT_2:44;
then A7: (r * L1) + (s * L2) is Linear_Combination of A by RLVECT_2:38;
assume A8: r + s = 1 ; ::_thesis: (r * v1) + (s * v2) in Affin A
sum ((r * L1) + (s * L2)) = (sum (r * L1)) + (sum (s * L2)) by Th34
.= (r * (sum L1)) + (sum (s * L2)) by Th35
.= (r * 1) + (s * 1) by A3, A5, Th35
.= 1 by A8 ;
hence  (r * v1) + (s * v2) in Affin A by A1, A7, A6; ::_thesis: verum
end;

theorem Th79: :: RLAFFIN1:79
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B holds
card A <= card B
proof
let V be RealLinearSpace; ::_thesis: for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B holds
card A <= card B
let A, B be finite Subset of V; ::_thesis: ( A is affinely-independent & Affin A c= Affin B implies card A <= card B )
assume that
A1: A is affinely-independent and
A2: Affin A c= Affin B ; ::_thesis: card A <= card B
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: card A <= card B
hence  card A <= card B ; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: card A <= card B
then consider p being set  such that
A3: p in A by XBOOLE_0:def_1;
reconsider p = p as Element of V by A3;
A4: A c= Affin A by Lm7;
then A5: p in Affin A by A3;
set LA = Lin ((- p) + A);
A6: card A = card ((- p) + A) by Th7;
 {} V c= B by XBOOLE_1:2;
then consider Ib being affinely-independent Subset of V such that
 {} V c= Ib and
A7: Ib c= B and
A8: Affin Ib = Affin B by Th60;
 not Ib is empty by A2, A3, A8;
then consider q being set  such that
A9: q in Ib by XBOOLE_0:def_1;
reconsider q = q as Element of V by A9;
set LI = Lin ((- q) + Ib);
A10: card Ib = card ((- q) + Ib) by Th7;
 (- q) + Ib c= the carrier of (Lin ((- q) + Ib))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- q) + Ib or x in the carrier of (Lin ((- q) + Ib)) )
assume  x in (- q) + Ib ; ::_thesis: x in the carrier of (Lin ((- q) + Ib))
then  x in Lin ((- q) + Ib) by RLVECT_3:15;
hence  x in the carrier of (Lin ((- q) + Ib)) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider qI = (- q) + Ib as finite Subset of (Lin ((- q) + Ib)) by A7, A10;
 (- q) + q = 0. V by RLVECT_1:5;
then A11: 0. V in qI by A9;
then A12: Lin ((- q) + Ib) = Lin ((((- q) + Ib) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116
.= Lin (((- q) + Ib) \ {(0. V)}) by Lm9
.= Lin (qI \ {(0. V)}) by RLVECT_5:20 ;
A13: ((- q) + Ib) \ {(0. V)} is linearly-independent by A9, Th41;
then  qI \ {(0. V)} is linearly-independent by RLVECT_5:15;
then  qI \ {(0. V)} is Basis of Lin ((- q) + Ib) by A12, RLVECT_3:def_3;
then reconsider LI = Lin ((- q) + Ib) as finite-dimensional Subspace of V by RLVECT_5:def_1;
A14: Ib c= Affin Ib by Lm7;
then A15: Affin Ib = q + (Up LI) by A9, Th57;
A16: Affin A = p + (Up (Lin ((- p) + A))) by A3, A4, Th57;
 (- p) + A c= the carrier of LI
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- p) + A or x in the carrier of LI )
A17: 2 + (- 1) = 1 ;
(2 * q) + ((- 1) * p) = ((1 + 1) * q) + ((- 1) * p)
.= ((1 * q) + (1 * q)) + ((- 1) * p) by RLVECT_1:def_6
.= ((1 * q) + (1 * q)) + (- p) by RLVECT_1:16
.= ((1 * q) + q) + (- p) by RLVECT_1:def_8
.= (q + q) + (- p) by RLVECT_1:def_8
.= (q + q) - p by RLVECT_1:def_11
.= (q - p) + q by RLVECT_1:28 ;
then  ( q + (Up LI) = q + LI & (q - p) + q in q + (Up LI) ) by A2, A8, A5, A9, A14, A15, A17, Th78, RUSUB_4:30;
then A18: q - p in LI by RLSUB_1:61;
assume  x in (- p) + A ; ::_thesis: x in the carrier of LI
then A19: x in Lin ((- p) + A) by RLVECT_3:15;
then  x in V by RLSUB_1:9;
then reconsider w = x as Element of V by STRUCT_0:def_5;
 w in Up (Lin ((- p) + A)) by A19, STRUCT_0:def_5;
then  p + w in Affin A by A16;
then  p + w in q + (Up LI) by A2, A8, A15;
then consider u being Element of V such that
A20: p + w = q + u and
A21: u in Up LI ;
A22: w = (q + u) - p by A20, RLVECT_4:1
.= q + (u - p) by RLVECT_1:28
.= u - (p - q) by RLVECT_1:29
.= u + (- (p - q)) by RLVECT_1:def_11
.= u + (q + (- p)) by RLVECT_1:33
.= u + (q - p) by RLVECT_1:def_11 ;
 u in LI by A21, STRUCT_0:def_5;
then  w in LI by A18, A22, RLSUB_1:20;
hence  x in the carrier of LI by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider LA = Lin ((- p) + A) as Subspace of LI by RLVECT_5:19;
 (- p) + A c= the carrier of LA
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (- p) + A or x in the carrier of LA )
assume  x in (- p) + A ; ::_thesis: x in the carrier of LA
then  x in LA by RLVECT_3:15;
hence  x in the carrier of LA by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider pA = (- p) + A as finite Subset of LA by A6;
 (- p) + p = 0. V by RLVECT_1:5;
then A23: 0. V in pA by A3;
then A24: {(0. V)} c= pA by ZFMISC_1:31;
A25: ((- p) + A) \ {(0. V)} is linearly-independent by A1, A3, Th41;
A26: card {(0. V)} = 1 by CARD_1:30;
A27: {(0. V)} c= qI by A11, ZFMISC_1:31;
A28: dim LI = card (qI \ {(0. V)}) by A13, A12, RLVECT_5:15, RLVECT_5:29
.= (card qI) - 1 by A27, A26, CARD_2:44 ;
Lin ((- p) + A) = Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}) by A23, ZFMISC_1:116
.= Lin (((- p) + A) \ {(0. V)}) by Lm9
.= Lin (pA \ {(0. V)}) by RLVECT_5:20 ;
then  dim LA = card (pA \ {(0. V)}) by A25, RLVECT_5:15, RLVECT_5:29
.= (card A) - 1 by A6, A26, A24, CARD_2:44 ;
then  (card A) - 1 <= (card qI) - 1 by A28, RLVECT_5:28;
then A29: card A <= card qI by XREAL_1:9;
 card qI <= card B by A7, A10, NAT_1:43;
hence  card A <= card B by A29, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

theorem :: RLAFFIN1:80
for V being RealLinearSpace
for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B & card A = card B holds
B is affinely-independent
proof
let V be RealLinearSpace; ::_thesis: for A, B being finite Subset of V st A is affinely-independent & Affin A c= Affin B & card A = card B holds
B is affinely-independent
let A, B be finite Subset of V; ::_thesis: ( A is affinely-independent & Affin A c= Affin B & card A = card B implies B is affinely-independent )
assume A1: ( A is affinely-independent & Affin A c= Affin B & card A = card B ) ; ::_thesis: B is affinely-independent
 {} V c= B by XBOOLE_1:2;
then consider Ib being affinely-independent Subset of V such that
 {} V c= Ib and
A2: Ib c= B and
A3: Affin Ib = Affin B by Th60;
reconsider IB = Ib as finite Subset of V by A2;
A4: card IB <= card B by A3, Th79;
 card B <= card IB by A1, A3, Th79;
hence  B is affinely-independent by A2, A4, CARD_FIN:1, XXREAL_0:1; ::_thesis: verum
end;

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)) )
proof
let r, s be Real; ::_thesis: 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)) )
let V be RealLinearSpace; ::_thesis: 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)) )
let v be VECTOR of V; ::_thesis: 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)) )
let L1, L2 be Linear_Combination of V; ::_thesis: ( L1 . v <> L2 . v implies ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) )
set u1 = L1 . v;
set u2 = L2 . v;
A1: ((r * L1) + ((1 - r) * L2)) . v = ((r * L1) . v) + (((1 - r) * L2) . v) by RLVECT_2:def_10
.= (r * (L1 . v)) + (((1 - r) * L2) . v) by RLVECT_2:def_11
.= (r * (L1 . v)) + (((- r) + 1) * (L2 . v)) by RLVECT_2:def_11
.= (r * ((L1 . v) - (L2 . v))) + (L2 . v) ;
assume A2: L1 . v <> L2 . v ; ::_thesis: ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
then A3: (L1 . v) - (L2 . v) <> 0 ;
A4: (L2 . v) - (L1 . v) <> 0 by A2;
hereby  ::_thesis: ( r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) implies ((r * L1) + ((1 - r) * L2)) . v = s )
assume  ((r * L1) + ((1 - r) * L2)) . v = s ; ::_thesis: r = ((L2 . v) - s) / ((L2 . v) - (L1 . v))
then  r * ((L2 . v) - (L1 . v)) = ((L2 . v) - s) * 1 by A1;
then  r / 1 = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) by A4, XCMPLX_1:94;
hence  r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ; ::_thesis: verum
end;
assume  r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ; ::_thesis: ((r * L1) + ((1 - r) * L2)) . v = s
hence ((r * L1) + ((1 - r) * L2)) . v = ((((L2 . v) - s) / (- ((L1 . v) - (L2 . v)))) * ((L1 . v) - (L2 . v))) + (L2 . v) by A1
.= (((- ((L2 . v) - s)) / ((L1 . v) - (L2 . v))) * ((L1 . v) - (L2 . v))) + (L2 . v) by XCMPLX_1:192
.= (- ((L2 . v) - s)) + (L2 . v) by A3, XCMPLX_1:87
.= s ;
::_thesis: verum
end;

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 & ( v in A or not v in Affin A ) ) )
proof
let V be RealLinearSpace; ::_thesis: for v being VECTOR of V
for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
let v be VECTOR of V; ::_thesis: for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
let A be Subset of V; ::_thesis: ( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
set Av = A \/ {v};
 v in {v} by TARSKI:def_1;
then A1: v in A \/ {v} by XBOOLE_0:def_3;
A2: A c= A \/ {v} by XBOOLE_1:7;
hereby  ::_thesis: ( A is affinely-independent & ( v in A or not v in Affin A ) implies A \/ {v} is affinely-independent )
assume A3: A \/ {v} is affinely-independent ; ::_thesis: ( A is affinely-independent & ( v in A or not v in Affin A ) )
hence  A is affinely-independent by Th43, XBOOLE_1:7; ::_thesis: ( v in A or not v in Affin A )
 ( v in Affin A implies v in A )
proof
assume  v in Affin A ; ::_thesis: v in A
then  {v} c= Affin A by ZFMISC_1:31;
then  Affin (A \/ {v}) = Affin A by Th69;
hence  v in A by A2, A1, A3, Th58; ::_thesis: verum
end;
hence  ( v in A or not v in Affin A ) ; ::_thesis: verum
end;
assume that
A4: A is affinely-independent and
A5: ( v in A or not v in Affin A ) ; ::_thesis: A \/ {v} is affinely-independent
percases ( v in A or ( not v in Affin A & not v in A ) ) by A5;
suppose v in A ; ::_thesis: A \/ {v} is affinely-independent
hence  A \/ {v} is affinely-independent by A4, ZFMISC_1:40; ::_thesis: verum
end;
supposeA6: ( not v in Affin A & not v in A ) ; ::_thesis: A \/ {v} is affinely-independent
consider I being affinely-independent Subset of V such that
A7: A c= I and
A8: I c= A \/ {v} and
A9: Affin I = Affin (A \/ {v}) by A2, A4, Th60;
assume A10: not A \/ {v} is affinely-independent ; ::_thesis: contradiction
 not v in I
proof
assume  v in I ; ::_thesis: contradiction
then  {v} c= I by ZFMISC_1:31;
hence  contradiction by A7, A10, Th43, XBOOLE_1:8; ::_thesis: verum
end;
then A11: I c= (A \/ {v}) \ {v} by A8, ZFMISC_1:34;
A12: A \/ {v} c= Affin (A \/ {v}) by Lm7;
 (A \/ {v}) \ {v} = A by A6, ZFMISC_1:117;
then  I = A by A7, A11, XBOOLE_0:def_10;
hence  contradiction by A1, A6, A9, A12; ::_thesis: verum
end;
end;
end;

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 & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
proof
let r, s be Real; ::_thesis: for V being RealLinearSpace
for w, v1, v2 being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let V be RealLinearSpace; ::_thesis: for w, v1, v2 being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let w, v1, v2 be VECTOR of V; ::_thesis: for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let A be Subset of V; ::_thesis: ( not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) implies ( r = s & v1 = v2 ) )
assume that
A1: ( not w in Affin A & v1 in A & v2 in A ) and
A2: r <> 1 and
A3: (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) ; ::_thesis: ( r = s & v1 = v2 )
r * w = (r * w) + (0. V) by RLVECT_1:4
.= (r * w) + (((1 - r) * v1) - ((1 - r) * v1)) by RLVECT_1:15
.= ((s * w) + ((1 - s) * v2)) - ((1 - r) * v1) by A3, RLVECT_1:28
.= (((1 - s) * v2) - ((1 - r) * v1)) + (s * w) by RLVECT_1:28 ;
then  (r * w) - (s * w) = ((1 - s) * v2) - ((1 - r) * v1) by RLVECT_4:1;
then A4: (r - s) * w = ((1 - s) * v2) - ((1 - r) * v1) by RLVECT_1:35;
A5: A c= Affin A by Lm7;
percases ( r <> s or r = s ) ;
suppose r <> s ; ::_thesis: ( r = s & v1 = v2 )
then A6: r - s <> 0 ;
A7: (1 / (r - s)) * (1 - s) = ((r - s) - (r - 1)) / (r - s) by XCMPLX_1:99
.= ((r - s) / (r - s)) - ((r - 1) / (r - s)) by XCMPLX_1:120
.= 1 - ((r - 1) / (r - s)) by A6, XCMPLX_1:60 ;
A8: - ((1 / (r - s)) * (1 - r)) = - ((1 - r) / (r - s)) by XCMPLX_1:99
.= (- (1 - r)) / (r - s) by XCMPLX_1:187 ;
 1 = (r - s) * (1 / (r - s)) by A6, XCMPLX_1:106;
then w = ((1 / (r - s)) * (r - s)) * w by RLVECT_1:def_8
.= (1 / (r - s)) * ((r - s) * w) by RLVECT_1:def_7
.= ((1 / (r - s)) * ((1 - s) * v2)) - ((1 / (r - s)) * ((1 - r) * v1)) by A4, RLVECT_1:34
.= (((1 / (r - s)) * (1 - s)) * v2) - ((1 / (r - s)) * ((1 - r) * v1)) by RLVECT_1:def_7
.= (((1 / (r - s)) * (1 - s)) * v2) - (((1 / (r - s)) * (1 - r)) * v1) by RLVECT_1:def_7
.= (((1 / (r - s)) * (1 - s)) * v2) + (- (((1 / (r - s)) * (1 - r)) * v1)) by RLVECT_1:def_11
.= ((1 - ((r - 1) / (r - s))) * v2) + (((r - 1) / (r - s)) * v1) by A7, A8, RLVECT_4:3 ;
hence  ( r = s & v1 = v2 ) by A1, A5, RUSUB_4:def_4; ::_thesis: verum
end;
supposeA9: r = s ; ::_thesis: ( r = s & v1 = v2 )
A10: 1 - r <> 0 by A2;
 (1 - r) * v1 = (1 - r) * v2 by A3, A9, RLVECT_1:8;
hence  ( r = s & v1 = v2 ) by A9, A10, RLVECT_1:36; ::_thesis: verum
end;
end;
end;

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 & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
proof
let r be Real; ::_thesis: for V being RealLinearSpace
for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
let V be RealLinearSpace; ::_thesis: for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
let v, w, p be VECTOR of V; ::_thesis: for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v
let I be affinely-independent Subset of V; ::_thesis: ( v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) implies r = (w |-- I) . v )
assume that
A1: v in I and
 w in Affin I and
A2: p in Affin (I \ {v}) and
A3: w = (r * v) + ((1 - r) * p) ; ::_thesis: r = (w |-- I) . v
A4: I c= conv I by CONVEX1:41;
 Carrier (p |-- (I \ {v})) c= I \ {v} by RLVECT_2:def_6;
then  not v in Carrier (p |-- (I \ {v})) by ZFMISC_1:56;
then A5: (p |-- (I \ {v})) . v = 0 ;
 I \ {v} c= I by XBOOLE_1:36;
then  ( Affin (I \ {v}) c= Affin I & I c= Affin I ) by Lm7, Th52;
hence (w |-- I) . v = (((1 - r) * (p |-- I)) + (r * (v |-- I))) . v by A1, A2, A3, Th70
.= (((1 - r) * (p |-- I)) . v) + ((r * (v |-- I)) . v) by RLVECT_2:def_10
.= (((1 - r) * (p |-- I)) . v) + (r * ((v |-- I) . v)) by RLVECT_2:def_11
.= ((1 - r) * ((p |-- I) . v)) + (r * ((v |-- I) . v)) by RLVECT_2:def_11
.= ((1 - r) * ((p |-- I) . v)) + (r * 1) by A1, A4, Th72
.= ((1 - r) * ((p |-- (I \ {v})) . v)) + (r * 1) by A2, Th77, XBOOLE_1:36
.= r by A5 ;
::_thesis: verum
end;