let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal F,(0. K) holds
for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal F,(0. K) holds
for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal F,(0. K) holds
for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let B2 be FinSequence of V2; :: thesis: for M being Matrix of len b1, len B2,K
for F being FinSequence_of_Matrix of K st M = block_diagonal F,(0. K) holds
for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let M be Matrix of len b1, len B2,K; :: thesis: for F being FinSequence_of_Matrix of K st M = block_diagonal F,(0. K) holds
for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
let F be FinSequence_of_Matrix of K; :: thesis: ( M = block_diagonal F,(0. K) implies for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) ) )
assume A1: M = block_diagonal F,(0. K) ; :: thesis: for i, m being Nat st i in dom b1 & m = min (Len F),i holds
( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
set B = block_diagonal F,(0. K);
let i, m be Nat; :: thesis: ( i in dom b1 & m = min (Len F),i implies ( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) ) )
assume A2: ( i in dom b1 & m = min (Len F),i ) ; :: thesis: ( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) )
A3: ( 1 <= i & i <= len b1 ) by A2, FINSEQ_3:27;
set ONE = 1. K,(len b1);
len (1. K,(len b1)) = len b1 by MATRIX_1:def 3;
then A4: ( dom (1. K,(len b1)) = dom b1 & width (1. K,(len b1)) = len b1 & len M = len b1 & dom b1 = Seg (len b1) & len M = Sum (Len F) & width M = Sum (Width F) & width M = len B2 ) by A3, A1, FINSEQ_1:def 3, FINSEQ_3:31, MATRIXJ1:def 5, MATRIX_1:24;
set W = Width F;
set L = Len F;
set Wm = Sum ((Width F) | m);
set Wm1 = Sum ((Width F) | (m -' 1));
set Fm = F . m;
set B2W = B2 | (Sum ((Width F) | m));
( m in dom (Len F) & dom (Len F) = dom F & dom (Width F) = dom F ) by A2, A4, MATRIXJ1:def 1, MATRIXJ1:def 3, MATRIXJ1:def 4;
then A5: ( 1 <= m & m <= len (Width F) & (Width F) . m = width (F . m) & m in NAT ) by FINSEQ_3:27, MATRIXJ1:def 4;
Width F = ((Width F) | m) ^ ((Width F) /^ m) by RFINSEQ:21;
then A6: Sum (Width F) = (Sum ((Width F) | m)) + (Sum ((Width F) /^ m)) by RVSUM_1:105;
A8: (Sum (Width F)) -' (Sum ((Width F) | m)) = (Sum (Width F)) - (Sum ((Width F) | m)) by A6, NAT_1:11, XREAL_1:235
.= Sum ((Width F) /^ m) by A6 ;
Width F = (((Width F) | (m -' 1)) ^ <*(width (F . m))*>) ^ ((Width F) /^ m) by A5, POLYNOM4:3;
then A9: Sum (Width F) = (Sum (((Width F) | (m -' 1)) ^ <*(width (F . m))*>)) + (Sum ((Width F) /^ m)) by RVSUM_1:105
.= ((Sum ((Width F) | (m -' 1))) + (width (F . m))) + (Sum ((Width F) /^ m)) by RVSUM_1:104 ;
then aa: Sum (Width F) = (Sum ((Width F) | (m -' 1))) + ((width (F . m)) + (Sum ((Width F) /^ m))) ;
A11: B2 = (B2 | (Sum ((Width F) | m))) ^ (B2 /^ (Sum ((Width F) | m))) by RFINSEQ:21;
then A12: ( len B2 = (len (B2 | (Sum ((Width F) | m)))) + (len (B2 /^ (Sum ((Width F) | m)))) & len (B2 | (Sum ((Width F) | m))) = Sum ((Width F) | m) ) by A4, A6, FINSEQ_1:35, FINSEQ_1:80, NAT_1:11;
Sum ((Width F) | m) >= Sum ((Width F) | (m -' 1)) by A6, A9, NAT_1:11;
then Seg (Sum ((Width F) | (m -' 1))) c= Seg (Sum ((Width F) | m)) by FINSEQ_1:7;
then (B2 | (Sum ((Width F) | m))) | (Sum ((Width F) | (m -' 1))) = B2 | (Sum ((Width F) | (m -' 1))) by RELAT_1:103;
then A13: B2 | (Sum ((Width F) | m)) = (B2 | (Sum ((Width F) | (m -' 1)))) ^ ((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))) by RFINSEQ:21;
then A14: ( len (B2 | (Sum ((Width F) | m))) = (len (B2 | (Sum ((Width F) | (m -' 1))))) + (len ((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1))))) & len (B2 | (Sum ((Width F) | (m -' 1)))) = Sum ((Width F) | (m -' 1)) ) by A4, aa, FINSEQ_1:35, FINSEQ_1:80, NAT_1:11;
A15: (B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1))) = (B2 | (Sum (Width (F | m)))) /^ (Sum ((Width F) | (m -' 1))) by MATRIXJ1:21
.= (B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))) by MATRIXJ1:21 ;
A16: ( len ((Sum ((Width F) | (m -' 1))) |-> (0. K)) = Sum ((Width F) | (m -' 1)) & len (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))) = width (F . m) & len (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)) = Sum ((Width F) /^ m) ) by A8, FINSEQ_1:def 18;
A17: len (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))) = Sum ((Width F) | m) by A6, A9, FINSEQ_1:def 18;
(Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line ((LineVec2Mx ((b1 /. i) |-- b1)) * M),1),B2) by MATRLIN2:def 3
.= Sum (lmlt (Line ((LineVec2Mx (Line (1. K,(len b1)),i)) * M),1),B2) by A2, MATRLIN2:19
.= Sum (lmlt (Line (LineVec2Mx (Line ((1. K,(len b1)) * M),i)),1),B2) by A2, A4, MATRLIN2:35
.= Sum (lmlt (Line (LineVec2Mx (Line M,i)),1),B2) by A4, MATRIXR2:68
.= Sum (lmlt (Line M,i),B2) by MATRIX15:25
.= Sum (lmlt ((((Sum (Width (F | (m -' 1)))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> (0. K))),B2) by A1, A2, A4, MATRIXJ1:37
.= Sum (lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))) ^ (((Sum (Width F)) -' (Sum (Width (F | m)))) |-> (0. K))),B2) by MATRIXJ1:21
.= Sum (lmlt ((((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))) ^ (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K))),B2) by MATRIXJ1:21
.= Sum ((lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))),(B2 | (Sum ((Width F) | m)))) ^ (lmlt (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)),(B2 /^ (Sum ((Width F) | m))))) by A4, A6, A16, A17, A11, A12, MATRLIN2:9
.= (Sum (lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))),(B2 | (Sum ((Width F) | m))))) + (Sum (lmlt (((Sum (Width F)) -' (Sum ((Width F) | m))) |-> (0. K)),(B2 /^ (Sum ((Width F) | m))))) by RLVECT_1:58
.= (Sum (lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))),(B2 | (Sum ((Width F) | m))))) + ((0. K) * (Sum (B2 /^ (Sum ((Width F) | m))))) by A4, A6, A8, A12, MATRLIN2:11
.= (Sum (lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))),(B2 | (Sum ((Width F) | m))))) + (0. V2) by VECTSP_1:59
.= Sum (lmlt (((Sum ((Width F) | (m -' 1))) |-> (0. K)) ^ (Line (F . m),(i -' (Sum (Len (F | (m -' 1))))))),(B2 | (Sum ((Width F) | m)))) by RLVECT_1:def 7
.= Sum ((lmlt ((Sum ((Width F) | (m -' 1))) |-> (0. K)),(B2 | (Sum ((Width F) | (m -' 1))))) ^ (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))) by A13, A14, A6, A9, A12, A16, MATRLIN2:9
.= (Sum (lmlt ((Sum ((Width F) | (m -' 1))) |-> (0. K)),(B2 | (Sum ((Width F) | (m -' 1)))))) + (Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))) by RLVECT_1:58
.= ((0. K) * (Sum (B2 | (Sum ((Width F) | (m -' 1)))))) + (Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))) by A14, MATRLIN2:11
.= (0. V2) + (Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1)))))) by VECTSP_1:59
.= Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum ((Width F) | m))) /^ (Sum ((Width F) | (m -' 1))))) by RLVECT_1:def 7 ;
hence ( (Mx2Tran M,b1,B2) . (b1 /. i) = Sum (lmlt (Line (F . m),(i -' (Sum (Len (F | (m -' 1)))))),((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1)))))) & len ((B2 | (Sum (Width (F | m)))) /^ (Sum (Width (F | (m -' 1))))) = width (F . m) ) by A15, A14, A6, A9, A12; :: thesis: verum