theorem Th1: :: RUSUB_3:1

for V being RealUnitarySpace
for A being Subset of V
for x being object holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )