theorem Th22: :: ENTROPY1:22

for p being non empty FinSequence of REAL
for q being FinSequence of REAL
for M being Matrix of REAL holds
( M = (ColVec2Mx p) * (LineVec2Mx q) iff ( len M = len p & width M = len q & ( for i being Nat st i in dom M holds
Line (M,i) = (p . i) * q ) ) )