theorem Th8: :: MATRLIN:8

for K being Field
for V being VectSp of K
for W being Element of V
for b2 being Basis of V ex KL being Linear_Combination of V st
( W = Sum KL & Carrier KL c= b2 )