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 } ;

per cases ( A is empty or not A is empty ) ;

suppose A1: 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 object such that
A2: x in { (Sum L) where L is Linear_Combination of A : sum L = 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 object such that
A4: p in A ;
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 object ; :: 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;
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;
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;
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))
.= p + (v + (0. V)) by RLVECT_1:def 8
.= x by A6 ;
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 object ; :: 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)) ;
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 ;
hence x in Affin A by A5, A21; :: thesis: verum

end;

end;