theorem Th20: :: MATRIX14:20

for K being Field
for x being FinSequence of K holds |(x,(0* (K,(len x))))| = 0. K