let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds dom (lmlt (p,R)) = (dom p) /\ (dom R)
let V1 be finite-dimensional VectSp of K; :: thesis: for R being FinSequence of V1
for p being FinSequence of K holds dom (lmlt (p,R)) = (dom p) /\ (dom R)
let R be FinSequence of V1; :: thesis: for p being FinSequence of K holds dom (lmlt (p,R)) = (dom p) /\ (dom R)
let p be FinSequence of K; :: thesis: dom (lmlt (p,R)) = (dom p) /\ (dom R)
( rng p c= the carrier of K & rng R c= the carrier of V1 ) by FINSEQ_1:def 4;
then [:(rng p),(rng R):] c= [: the carrier of K, the carrier of V1:] by ZFMISC_1:96;
then [:(rng p),(rng R):] c= dom the lmult of V1 by FUNCT_2:def 1;
hence dom (lmlt (p,R)) = (dom p) /\ (dom R) by FUNCOP_1:69; :: thesis: verum