Affin A = { (Sum L) where L is Linear_Combination of A : sum L = 1 } by Th59;
hence ex b₁ being Linear_Combination of A st
( Sum b₁ = x & sum b₁ = 1 ) by A2; :: thesis: verum