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) ) )
A2: mlt f1,f2 = the multF of K .: f1,f2 by FVSUM_1:def 7;
A4: dom the multF of K = [:the carrier of K,the carrier of K:] by FUNCT_2:def 1;
A5: rng f1 c= the carrier of K by FINSEQ_1:def 4;
rng f2 c= the carrier of K by FINSEQ_1:def 4;
then [:(rng f1),(rng f2):] c= dom the multF of K by A5, A4, ZFMISC_1:119;
hence dom (mlt f1,f2) = (dom f1) /\ (dom f2) by A2, 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 FV73; :: thesis: verum