for r being Real
for V being RealLinearSpace
for Af being finite Subset of V ex L being Linear_Combination of Af st
( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )