theorem Th20: :: ENTROPY1:20

for p being FinSequence of REAL
for j being Nat st j in dom p holds
Col ((LineVec2Mx p),j) = <*(p . j)*>