let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for a, d being FinSequence of K st len a = len b1 holds
for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for a, d being FinSequence of K st len a = len b1 holds
for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for a, d being FinSequence of K st len a = len b1 holds
for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for a, d being FinSequence of K st len a = len b1 holds
for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
let b2 be OrdBasis of V2; :: thesis: for a, d being FinSequence of K st len a = len b1 holds
for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
let a, d be FinSequence of K; :: thesis: ( len a = len b1 implies for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) )
assume A1: len a = len b1 ; :: thesis: for j being Nat st j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 holds
((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
reconsider B3 = f * b1 as FinSequence of V2 ;
deffunc H₁( Nat, Nat) -> Element of the carrier of K = ((B3 /. $1) |-- b2) /. $2;
consider M being Matrix of len b1, len b2, the carrier of K such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H₁(i,j) from MATRIX_0:sch 1();
deffunc H₂( Nat) -> Element of the carrier of K = Sum (mlt (a,(Col (M,$1))));
consider dd being FinSequence of K such that
A3: ( len dd = len b2 & ( for j being Nat st j in dom dd holds
dd /. j = H₂(j) ) ) from FINSEQ_4:sch 2();
let j be Nat; :: thesis: ( j in dom b2 & len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) & len b1 > 0 implies ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) )
assume A4: j in dom b2 ; :: thesis: ( not len d = len b1 or ex k being Nat st
( k in dom b1 & not d . k = ((f . (b1 /. k)) |-- b2) /. j ) or not len b1 > 0 or ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) )
A5: j in dom dd by A4, A3, FINSEQ_3:29;
assume that
A6: len d = len b1 and
A7: for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ; :: thesis: ( not len b1 > 0 or ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d)) )
A8: len (Col (M,j)) = len M by MATRIX_0:def 8
.= len d by A6, MATRIX_0:def 2 ;
len M = len b1 by MATRIX_0:def 2;
then A9: dom M = dom b1 by FINSEQ_3:29;
A10: len b1 = len B3 by FINSEQ_2:33;
then A11: dom b1 = dom B3 by FINSEQ_3:29;
assume A12: len b1 > 0 ; :: thesis: ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = Sum (mlt (a,d))
then A13: width M = len b2 by MATRIX_0:23;

A14: now :: thesis: for i being Nat st i in dom B3 holds
B3 /. i = Sum (lmlt ((Line (M,i)),b2))

let i be Nat; :: thesis: ( i in dom B3 implies B3 /. i = Sum (lmlt ((Line (M,i)),b2)) )
assume A15: i in dom B3 ; :: thesis: B3 /. i = Sum (lmlt ((Line (M,i)),b2))

A16: now :: thesis: for j being Nat st j in dom ((B3 /. i) |-- b2) holds
(Line (M,i)) . j = ((B3 /. i) |-- b2) . j

let j be Nat; :: thesis: ( j in dom ((B3 /. i) |-- b2) implies (Line (M,i)) . j = ((B3 /. i) |-- b2) . j )
assume A17: j in dom ((B3 /. i) |-- b2) ; :: thesis: (Line (M,i)) . j = ((B3 /. i) |-- b2) . j
then j in Seg (len ((B3 /. i) |-- b2)) by FINSEQ_1:def 3;
then A18: j in Seg (width M) by A13, Def7;
then [i,j] in [:(dom M),(Seg (width M)):] by A9, A11, A15, ZFMISC_1:87;
then A19: [i,j] in Indices M by MATRIX_0:def 4;
thus (Line (M,i)) . j = M * (i,j) by A18, MATRIX_0:def 7
.= ((B3 /. i) |-- b2) /. j by A2, A19
.= ((B3 /. i) |-- b2) . j by A17, PARTFUN1:def 6 ; :: thesis: verum

end;

A20: len (Line (M,i)) = width M by MATRIX_0:def 7
.= len ((B3 /. i) |-- b2) by A13, Def7 ;
thus B3 /. i = Sum (lmlt (((B3 /. i) |-- b2),b2)) by Th35
.= Sum (lmlt ((Line (M,i)),b2)) by A20, A16, FINSEQ_2:9 ; :: thesis: verum

end;

Seg (len b2) = dom b2 by FINSEQ_1:def 3;
then A21: j in Seg (width M) by A4, A12, MATRIX_0:23;

A22: now :: thesis: for i being Nat st i in dom d holds
(Col (M,j)) . i = d . i

let i be Nat; :: thesis: ( i in dom d implies (Col (M,j)) . i = d . i )
assume i in dom d ; :: thesis: (Col (M,j)) . i = d . i
then A23: i in dom b1 by A6, FINSEQ_3:29;
then A24: B3 /. i = B3 . i by A11, PARTFUN1:def 6
.= f . (b1 . i) by A23, FUNCT_1:13
.= f . (b1 /. i) by A23, PARTFUN1:def 6 ;
[i,j] in [:(dom M),(Seg (width M)):] by A9, A21, A23, ZFMISC_1:87;
then A25: [i,j] in Indices M by MATRIX_0:def 4;
thus (Col (M,j)) . i = M * (i,j) by A9, A23, MATRIX_0:def 8
.= ((f . (b1 /. i)) |-- b2) /. j by A2, A24, A25
.= d . i by A7, A23 ; :: thesis: verum

end;

len b2 > 0 by A4, Lm2;
hence ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = ((Sum (lmlt (dd,b2))) |-- b2) /. j by A1, A12, A3, A10, A14, Th33
.= dd /. j by A3, Th36
.= Sum (mlt (a,(Col (M,j)))) by A3, A5
.= Sum (mlt (a,d)) by A8, A22, FINSEQ_2:9 ;
:: thesis: verum