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 H1( 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) = H1(i,j) from deffunc H2( 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 = H2(j) ) ) from 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 ;
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 ;
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 () by ;
then [i,j] in [:(dom M),(Seg ()):] by ;
then A19: [i,j] in Indices M by MATRIX_0:def 4;
thus (Line (M,i)) . j = M * (i,j) by
.= ((B3 /. i) |-- b2) /. j by
.= ((B3 /. i) |-- b2) . j by ; :: thesis: verum
end;
A20: len (Line (M,i)) = width M by MATRIX_0:def 7
.= len ((B3 /. i) |-- b2) by ;
thus B3 /. i = Sum (lmlt (((B3 /. i) |-- b2),b2)) by Th35
.= Sum (lmlt ((Line (M,i)),b2)) by ; :: thesis: verum
end;
Seg (len b2) = dom b2 by FINSEQ_1:def 3;
then A21: j in Seg () by ;
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 ;
then A24: B3 /. i = B3 . i by
.= f . (b1 . i) by
.= f . (b1 /. i) by ;
[i,j] in [:(dom M),(Seg ()):] by ;
then A25: [i,j] in Indices M by MATRIX_0:def 4;
thus (Col (M,j)) . i = M * (i,j) by
.= ((f . (b1 /. i)) |-- b2) /. j by A2, A24, A25
.= d . i by ; :: thesis: verum
end;
len b2 > 0 by ;
hence ((Sum (lmlt (a,(f * b1)))) |-- b2) /. j = ((Sum (lmlt (dd,b2))) |-- b2) /. j by A1, A12, A3, A10, A14, Th33
.= dd /. j by
.= Sum (mlt (a,(Col (M,j)))) by A3, A5
.= Sum (mlt (a,d)) by ;
:: thesis: verum