theorem Th38: :: MATRIX11:38

for n, m being Nat
for D being non empty set
for M being Matrix of n,m,D
for F being Function of (Seg n),(Seg n)
for k being Nat st k in Seg n holds
Line ((M * F),k) = M . (F . k)