:: deftheorem Def4 defines circled CIRCLED1:def 4 :
for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is circled iff ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) ) );