for V being ComplexLinearSpace
for A being Subset of V st A <> {} holds
( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A )