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

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