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 & ( the multF of K is having_a_unity or ( len f1 >= 1 & len f2 >= 1 ) ) ) by GROUP_1:31, GROUP_1:34;
hence the multF of K $$ (f1 ^ f2) = (the multF of K $$ f1) * (the multF of K $$ f2) by FINSOP_1:6; :: thesis: verum