let K be Field; :: thesis: for f1, f2 being FinSequence of K holds the multF of K $$ (f1 ^ f2) = (the multF of K $$ f1) * (the multF of K $$ f2)
let f1, f2 be FinSequence of K; :: thesis: the multF of K $$ (f1 ^ f2) = (the multF of K $$ f1) * (the multF of K $$ f2)
the multF of K is associative by GROUP_1:31;
hence the multF of K $$ (f1 ^ f2) = (the multF of K $$ f1) * (the multF of K $$ f2) by FINSOP_1:6, GROUP_1:34; :: thesis: verum