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

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