let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for p2 being FinSequence of V1
for p1 being FinSequence of K st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1
let V1 be finite-dimensional VectSp of K; :: thesis: for p2 being FinSequence of V1
for p1 being FinSequence of K st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1
let p2 be FinSequence of V1; :: thesis: for p1 being FinSequence of K st dom p1 = dom p2 holds
dom (lmlt (p1,p2)) = dom p1
let p1 be FinSequence of K; :: thesis: ( dom p1 = dom p2 implies dom (lmlt (p1,p2)) = dom p1 )
assume A1: dom p1 = dom p2 ; :: thesis: dom (lmlt (p1,p2)) = dom p1
( rng p1 c= the carrier of K & rng p2 c= the carrier of V1 ) by FINSEQ_1:def 4;
then A2: [:(rng p1),(rng p2):] c= [: the carrier of K, the carrier of V1:] by ZFMISC_1:96;
( rng <:p1,p2:> c= [:(rng p1),(rng p2):] & [: the carrier of K, the carrier of V1:] = dom the lmult of V1 ) by FUNCT_2:def 1, FUNCT_3:51;
hence dom (lmlt (p1,p2)) = dom <:p1,p2:> by A2, RELAT_1:27, XBOOLE_1:1
.= (dom p1) /\ (dom p2) by FUNCT_3:def 7
.= dom p1 by A1 ;
:: thesis: verum