:: deftheorem defines * LAPLACE:def 9 :
for K being Field
for M being Matrix of K
for f being FinSequence of K holds M * f = M * (<*f*> @);