let j be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B1 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B1 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B1 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j
let b1 be OrdBasis of V1; :: thesis: for B1 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j
let B1 be FinSequence of V1; :: thesis: for p1, p2 being FinSequence of K st len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j
let p1, p2 be FinSequence of K; :: thesis: ( len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) implies p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j )
assume that
A1: len p1 = len p2 and
A2: len p1 = len B1 and
A3: len p1 > 0 and
A4: j in dom b1 and
A5: for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ; :: thesis: p1 "*" p2 = ((Sum (lmlt p1,B1)) |-- b1) . j
deffunc H₁( Nat, Nat) -> Element of the carrier of K = ((B1 /. $1) |-- b1) /. $2;
consider M being Matrix of len p1, len b1,K such that
A6: for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();
A7: len M = len p1 by A3, MATRIX_1:24;
then A8: dom p1 = dom M by FINSEQ_3:31;
A9: width M = len b1 by A3, MATRIX_1:24;
A10: dom b1 = Seg (len b1) by FINSEQ_1:def 3;
A11: dom p1 = Seg (len p1) by FINSEQ_1:def 3;
A12: dom p1 = dom p2 by A1, FINSEQ_3:31;

A13: now

let i be Nat; :: thesis: ( 1 <= i & i <= len p2 implies (Col M,j) . i = p2 . i )
assume ( 1 <= i & i <= len p2 ) ; :: thesis: (Col M,j) . i = p2 . i
then A14: i in dom p1 by A1, A11, FINSEQ_1:3;
then A15: [i,j] in Indices M by A4, A9, A8, A10, ZFMISC_1:106;
len ((B1 /. i) |-- b1) = len b1 by MATRLIN:def 9;
then A16: dom ((B1 /. i) |-- b1) = dom b1 by FINSEQ_3:31;
thus (Col M,j) . i = M * i,j by A8, A14, MATRIX_1:def 9
.= ((B1 /. i) |-- b1) /. j by A6, A15
.= ((B1 /. i) |-- b1) . j by A4, A16, PARTFUN1:def 8
.= p2 . i by A5, A12, A14 ; :: thesis: verum

end;

deffunc H₂( Nat) -> Element of the carrier of K = Sum (mlt p1,(Col M,$1));
consider MC being FinSequence of K such that
A17: ( len MC = len b1 & ( for j being Nat st j in dom MC holds
MC . j = H₂(j) ) ) from FINSEQ_2:sch 1();
A18: for j being Nat st j in dom MC holds
MC /. j = H₂(j)

proof

let j be Nat; :: thesis: ( j in dom MC implies MC /. j = H₂(j) )
assume A19: j in dom MC ; :: thesis: MC /. j = H₂(j)
then MC . j = H₂(j) by A17;
hence MC /. j = H₂(j) by A19, PARTFUN1:def 8; :: thesis: verum

end;

A20: dom b1 = dom MC by A17, FINSEQ_3:31;
A21: dom p1 = dom B1 by A2, FINSEQ_3:31;

A22: now

let i be Nat; :: thesis: ( i in dom B1 implies B1 /. i = Sum (lmlt (Line M,i),b1) )
assume A23: i in dom B1 ; :: thesis: B1 /. i = Sum (lmlt (Line M,i),b1)
A24: len (Line M,i) = width M by MATRIX_1:def 8;
len ((B1 /. i) |-- b1) = len b1 by MATRLIN:def 9;
then A25: dom (Line M,i) = dom ((B1 /. i) |-- b1) by A9, A24, FINSEQ_3:31;
A26: dom (Line M,i) = Seg (width M) by A24, FINSEQ_1:def 3;

A27: now

let k be Nat; :: thesis: ( k in dom ((B1 /. i) |-- b1) implies (Line M,i) . k = ((B1 /. i) |-- b1) . k )
assume A28: k in dom ((B1 /. i) |-- b1) ; :: thesis: (Line M,i) . k = ((B1 /. i) |-- b1) . k
A29: [i,k] in Indices M by A21, A8, A23, A25, A26, A28, ZFMISC_1:106;
thus (Line M,i) . k = M * i,k by A25, A26, A28, MATRIX_1:def 8
.= ((B1 /. i) |-- b1) /. k by A6, A29
.= ((B1 /. i) |-- b1) . k by A28, PARTFUN1:def 8 ; :: thesis: verum

end;

thus B1 /. i = Sum (lmlt ((B1 /. i) |-- b1),b1) by MATRLIN:40
.= Sum (lmlt (Line M,i),b1) by A25, A27, FINSEQ_1:17 ; :: thesis: verum

end;

A30: b1 <> {} by A4;
A31: len (Col M,j) = len M by FINSEQ_1:def 18;
len ((Sum (lmlt p1,B1)) |-- b1) = len b1 by MATRLIN:def 9;
then dom ((Sum (lmlt p1,B1)) |-- b1) = dom b1 by FINSEQ_3:31;
hence ((Sum (lmlt p1,B1)) |-- b1) . j = ((Sum (lmlt p1,B1)) |-- b1) /. j by A4, PARTFUN1:def 8
.= ((Sum (lmlt MC,b1)) |-- b1) /. j by A2, A3, A17, A18, A30, A22, MATRLIN:38
.= MC /. j by A17, MATRLIN:41
.= MC . j by A4, A20, PARTFUN1:def 8
.= Sum (mlt p1,(Col M,j)) by A4, A17, A20
.= p1 "*" p2 by A1, A7, A31, A13, FINSEQ_1:18 ;
:: thesis: verum