theorem :: MATRIX_7:30

for K being commutative Ring
for f1, f2 being FinSequence of K holds the multF of K $$ (f1 ^ f2) = ( the multF of K $$ f1) * ( the multF of K $$ f2) by FINSOP_1:5;