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