theorem Th8: :: ZMATRLIN:10

for V being free finite-rank Z_Module
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 )