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:96;
hence dom (mlt (f1,f2)) = (dom f1) /\ (dom f2) by FUNCOP_1:69; :: 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