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_0:sch 1();
A7: len M = len p1 by A3, MATRIX_0:23;
then A8: dom p1 = dom M by FINSEQ_3:29;
A9: width M = len b1 by A3, MATRIX_0:23;
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:29;

A13: now :: thesis: for i being Nat st 1 <= i & i <= len p2 holds
(Col (M,j)) . i = p2 . i

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;
then A15: [i,j] in Indices M by A4, A9, A8, A10, ZFMISC_1:87;
len ((B1 /. i) |-- b1) = len b1 by MATRLIN:def 7;
then A16: dom ((B1 /. i) |-- b1) = dom b1 by FINSEQ_3:29;
thus (Col (M,j)) . i = M * (i,j) by A8, A14, MATRIX_0:def 8
.= ((B1 /. i) |-- b1) /. j by A6, A15
.= ((B1 /. i) |-- b1) . j by A4, A16, PARTFUN1:def 6
.= 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 6; :: thesis: verum

end;

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

A22: now :: thesis: for i being Nat st i in dom B1 holds
B1 /. i = Sum (lmlt ((Line (M,i)),b1))

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_0:def 7;
len ((B1 /. i) |-- b1) = len b1 by MATRLIN:def 7;
then A25: dom (Line (M,i)) = dom ((B1 /. i) |-- b1) by A9, A24, FINSEQ_3:29;
A26: dom (Line (M,i)) = Seg (width M) by A24, FINSEQ_1:def 3;

A27: now :: thesis: for k being Nat st k in dom ((B1 /. i) |-- b1) holds
(Line (M,i)) . k = ((B1 /. i) |-- b1) . k

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:87;
thus (Line (M,i)) . k = M * (i,k) by A25, A26, A28, MATRIX_0:def 7
.= ((B1 /. i) |-- b1) /. k by A6, A29
.= ((B1 /. i) |-- b1) . k by A28, PARTFUN1:def 6 ; :: thesis: verum

end;

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

end;

A30: b1 <> {} by A4;
A31: len (Col (M,j)) = len M by CARD_1:def 7;
len ((Sum (lmlt (p1,B1))) |-- b1) = len b1 by MATRLIN:def 7;
then dom ((Sum (lmlt (p1,B1))) |-- b1) = dom b1 by FINSEQ_3:29;
hence ((Sum (lmlt (p1,B1))) |-- b1) . j = ((Sum (lmlt (p1,B1))) |-- b1) /. j by A4, PARTFUN1:def 6
.= ((Sum (lmlt (MC,b1))) |-- b1) /. j by A2, A3, A17, A18, A30, A22, MATRLIN:33
.= MC /. j by A17, MATRLIN:36
.= MC . j by A4, A20, PARTFUN1:def 6
.= Sum (mlt (p1,(Col (M,j)))) by A4, A17, A20
.= p1 "*" p2 by A1, A7, A31, A13, FINSEQ_1:14 ;
:: thesis: verum