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_1: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:31;
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_1:def 9
.= len d by A6, MATRIX_1:def 3 ;
len M = len b1 by MATRIX_1:def 3;
then A9: dom M = dom b1 by FINSEQ_3:31;
A10: len b1 = len B3 by FINSEQ_2:37;
then A11: dom b1 = dom B3 by FINSEQ_3:31;
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_1:24;

A14: now

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

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, Def9;
then [i,j] in [:(dom M),(Seg (width M)):] by A9, A11, A15, ZFMISC_1:106;
then A19: [i,j] in Indices M by MATRIX_1:def 5;
thus (Line M,i) . j = M * i,j by A18, MATRIX_1:def 8
.= ((B3 /. i) |-- b2) /. j by A2, A19
.= ((B3 /. i) |-- b2) . j by A17, PARTFUN1:def 8 ; :: thesis: verum

end;

A20: len (Line M,i) = width M by MATRIX_1:def 8
.= len ((B3 /. i) |-- b2) by A13, Def9 ;
thus B3 /. i = Sum (lmlt ((B3 /. i) |-- b2),b2) by Th40
.= Sum (lmlt (Line M,i),b2) by A20, A16, NEWTON:3 ; :: thesis: verum

end;

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

A22: now

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:31;
then A24: B3 /. i = B3 . i by A11, PARTFUN1:def 8
.= f . (b1 . i) by A23, FUNCT_1:23
.= f . (b1 /. i) by A23, PARTFUN1:def 8 ;
[i,j] in [:(dom M),(Seg (width M)):] by A9, A21, A23, ZFMISC_1:106;
then A25: [i,j] in Indices M by MATRIX_1:def 5;
thus (Col M,j) . i = M * i,j by A9, A23, MATRIX_1:def 9
.= ((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, Th38
.= dd /. j by A3, Th41
.= Sum (mlt a,(Col M,j)) by A3, A5
.= Sum (mlt a,d) by A8, A22, NEWTON:3 ;
:: thesis: verum