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_{1}( 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_{1}(i,j)
from MATRIX_0:sch 1();

deffunc H_{2}( 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_{2}(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;

then A21: j in Seg (width M) by A4, A12, MATRIX_0:23;

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

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

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

deffunc H

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

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))

Seg (len b2) = dom b2
by FINSEQ_1:def 3;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))

.= 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;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

A20: len (Line (M,i)) =
width M
by MATRIX_0:def 7
(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;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

.= 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

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

len b2 > 0
by A4, Lm2;(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;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

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