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 }