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:92;
reconsider r1 = R1 as Element of (len p1) -tuples_on the carrier of V1 by A1, FINSEQ_2:92;
reconsider P1 = p1 as Element of (len p1) -tuples_on the carrier of K by FINSEQ_2:92;
reconsider P2 = p2 as Element of (len p2) -tuples_on the carrier of K by FINSEQ_2:92;
thus lmlt ((p1 ^ p2),(R1 ^ R2)) = ( the lmult of V1 .: (P1,r1)) ^ ( the lmult of V1 .: (P2,r2)) by FINSEQOP:11
.= (lmlt (p1,R1)) ^ (lmlt (p2,R2)) ; :: thesis: verum