let K be Field; :: thesis:
let V1, V2 be finite-dimensional VectSp of K; :: thesis:
let f be Function of V1,V2; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let b2 be OrdBasis of V2; :: thesis:
let a, d be FinSequence of K; :: thesis:
assume A1: len a = len b1 ; :: thesis:
let j be Nat; :: thesis:
assume A2: j in dom b2 ; :: thesis:
A3: len b2 > 0 by A2, Lm2;
assume A4: ( len d = len b1 & ( for k being Nat st k in dom b1 holds
d . k = ((f . (b1 /. k)) |-- b2) /. j ) ) ; :: thesis:
assume A5: len b1 > 0 ; :: thesis:
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
A6: 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
A7: ( len dd = len b2 & ( for j being Nat st j in dom dd holds
dd /. j = H₂(j) ) ) from FINSEQ_4:sch 2();
A8: for j being Nat st j in dom dd holds
dd /. j = H₂(j) by A7;
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;
A12: len (Col M,j) = len M by MATRIX_1:def 9
.= len d by A4, MATRIX_1:def 3 ;
A13: Seg (len b2) = dom b2 by FINSEQ_1:def 3;
A14: width M = len b2 by A5, MATRIX_1:24;
A15: j in Seg (width M) by A2, A5, A13, MATRIX_1:24;

A16: now

let i be Nat; :: thesis:
assume i in dom d ; :: thesis:
then A17: i in dom b1 by A4, FINSEQ_3:31;
then A18: B3 /. i = B3 . i by A11, PARTFUN1:def 8
.= f . (b1 . i) by A17, FUNCT_1:23
.= f . (b1 /. i) by A17, PARTFUN1:def 8 ;
[i,j] in [:(dom M),(Seg (width M)):] by A9, A15, A17, ZFMISC_1:106;
then A19: [i,j] in Indices M by MATRIX_1:def 5;
thus (Col M,j) . i = M * i,j by A9, A17, MATRIX_1:def 9
.= ((f . (b1 /. i)) |-- b2) /. j by A6, A18, A19
.= d . i by A4, A17 ; :: thesis:

end;

A20: now

let i be Nat; :: thesis:
assume A21: i in dom B3 ; :: thesis:
A22: len (Line M,i) = width M by MATRIX_1:def 8
.= len ((B3 /. i) |-- b2) by A14, Def9 ;

A23: now

let j be Nat; :: thesis:
assume A24: j in dom ((B3 /. i) |-- b2) ; :: thesis:
then j in Seg (len ((B3 /. i) |-- b2)) by FINSEQ_1:def 3;
then A25: j in Seg (width M) by A14, Def9;
then [i,j] in [:(dom M),(Seg (width M)):] by A9, A11, A21, ZFMISC_1:106;
then A26: [i,j] in Indices M by MATRIX_1:def 5;
thus (Line M,i) . j = M * i,j by A25, MATRIX_1:def 8
.= ((B3 /. i) |-- b2) /. j by A6, A26
.= ((B3 /. i) |-- b2) . j by A24, PARTFUN1:def 8 ; :: thesis:

end;

thus B3 /. i = Sum (lmlt ((B3 /. i) |-- b2),b2) by Th40
.= Sum (lmlt (Line M,i),b2) by A22, A23, NEWTON:3 ; :: thesis:

end;

A27: j in dom dd by A2, A7, FINSEQ_3:31;
thus ((Sum (lmlt a,(f * b1))) |-- b2) /. j = ((Sum (lmlt dd,b2)) |-- b2) /. j by A1, A3, A5, A7, A10, A20, Th38
.= dd /. j by A7, Th41
.= Sum (mlt a,(Col M,j)) by A8, A27
.= Sum (mlt a,d) by A12, A16, NEWTON:3 ; :: thesis: