let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len R1 & len p2 = len R2 holds
lmlt (p1 ^ p2),(R1 ^ R2) = (lmlt p1,R1) ^ (lmlt p2,R2)
let V1 be finite-dimensional VectSp of K; :: thesis: for R1, R2 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len R1 & len p2 = len R2 holds
lmlt (p1 ^ p2),(R1 ^ R2) = (lmlt p1,R1) ^ (lmlt p2,R2)
let R1, R2 be FinSequence of V1; :: thesis: for p1, p2 being FinSequence of K st len p1 = len R1 & len p2 = len R2 holds
lmlt (p1 ^ p2),(R1 ^ R2) = (lmlt p1,R1) ^ (lmlt p2,R2)
let p1, p2 be FinSequence of K; :: thesis: ( len p1 = len R1 & len p2 = len R2 implies lmlt (p1 ^ p2),(R1 ^ R2) = (lmlt p1,R1) ^ (lmlt p2,R2) )
assume that
A1: len p1 = len R1 and
A2: len p2 = len R2 ; :: thesis: lmlt (p1 ^ p2),(R1 ^ R2) = (lmlt p1,R1) ^ (lmlt p2,R2)
reconsider r2 = R2 as Element of (len p2) -tuples_on the carrier of V1 by A2, FINSEQ_2:110;
reconsider r1 = R1 as Element of (len p1) -tuples_on the carrier of V1 by A1, FINSEQ_2:110;
reconsider P1 = p1 as Element of (len p1) -tuples_on the carrier of K by FINSEQ_2:110;
reconsider P2 = p2 as Element of (len p2) -tuples_on the carrier of K by FINSEQ_2:110;
thus lmlt (p1 ^ p2),(R1 ^ R2) = (the lmult of V1 .: P1,r1) ^ (the lmult of V1 .: P2,r2) by FINSEQOP:12
.= (lmlt p1,R1) ^ (lmlt p2,R2) ; :: thesis: verum