let K be Field; :: thesis: for f1, f2 being FinSequence of K holds
( dom (mlt f1,f2) = (dom f1) /\ (dom f2) & ( for i being Element of NAT st i in dom (mlt f1,f2) holds
(mlt f1,f2) . i = (f1 /. i) * (f2 /. i) ) )
let f1, f2 be FinSequence of K; :: thesis: ( dom (mlt f1,f2) = (dom f1) /\ (dom f2) & ( for i being Element of NAT st i in dom (mlt f1,f2) holds
(mlt f1,f2) . i = (f1 /. i) * (f2 /. i) ) )
A1: rng f2 c= the carrier of K by FINSEQ_1:def 4;
( dom the multF of K = [:the carrier of K,the carrier of K:] & rng f1 c= the carrier of K ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then ( mlt f1,f2 = the multF of K .: f1,f2 & [:(rng f1),(rng f2):] c= dom the multF of K ) by A1, FVSUM_1:def 7, ZFMISC_1:119;
hence dom (mlt f1,f2) = (dom f1) /\ (dom f2) by FUNCOP_1:84; :: thesis: for i being Element of NAT st i in dom (mlt f1,f2) holds
(mlt f1,f2) . i = (f1 /. i) * (f2 /. i)
thus for i being Element of NAT st i in dom (mlt f1,f2) holds
(mlt f1,f2) . i = (f1 /. i) * (f2 /. i) by Th4; :: thesis: verum