let i be Nat; :: thesis: for K being Field
for V1, V2 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for W1, W2 being Subspace of V1
for U1, U2 being Subspace of V2
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let W1, W2 be Subspace of V1; :: thesis: for U1, U2 being Subspace of V2
for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let U1, U2 be Subspace of V2; :: thesis: for b1 being OrdBasis of V1
for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let b1 be OrdBasis of V1; :: thesis: for B2 being FinSequence of V2
for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let B2 be FinSequence of V2; :: thesis: for bw1 being OrdBasis of W1
for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let bw1 be OrdBasis of W1; :: thesis: for bw2 being OrdBasis of W2
for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let bw2 be OrdBasis of W2; :: thesis: for Bu1 being FinSequence of U1
for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let Bu1 be FinSequence of U1; :: thesis: for Bu2 being FinSequence of U2
for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let Bu2 be FinSequence of U2; :: thesis: for M being Matrix of len b1, len B2,K
for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let M be Matrix of len b1, len B2,K; :: thesis: for M1 being Matrix of len bw1, len Bu1,K
for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let M1 be Matrix of len bw1, len Bu1,K; :: thesis: for M2 being Matrix of len bw2, len Bu2,K st b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 holds
( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
let M2 be Matrix of len bw2, len Bu2,K; :: thesis: ( b1 = bw1 ^ bw2 & B2 = Bu1 ^ Bu2 & M = block_diagonal (<*M1,M2*>,(0. K)) & width M1 = len Bu1 & width M2 = len Bu2 implies ( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) ) )
assume that
A1: b1 = bw1 ^ bw2 and
A2: B2 = Bu1 ^ Bu2 and
A3: M = block_diagonal (<*M1,M2*>,(0. K)) and
A4: width M1 = len Bu1 and
A5: width M2 = len Bu2 ; :: thesis: ( ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) & ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) ) )
A6: dom bw1 c= dom b1 by A1, FINSEQ_1:26;
( rng Bu2 c= the carrier of U2 & the carrier of U2 c= the carrier of V2 ) by FINSEQ_1:def 4, VECTSP_4:def 2;
then A7: rng Bu2 c= the carrier of V2 ;
( rng Bu1 c= the carrier of U1 & the carrier of U1 c= the carrier of V2 ) by FINSEQ_1:def 4, VECTSP_4:def 2;
then rng Bu1 c= the carrier of V2 ;
then reconsider bu1 = Bu1, bu2 = Bu2 as FinSequence of V2 by A7, FINSEQ_1:def 4;
set F1 = Mx2Tran (M1,bw1,Bu1);
set F = Mx2Tran (M,b1,B2);
A8: ( dom b1 = Seg (len b1) & len (1. (K,(len b1))) = len b1 ) by FINSEQ_1:def 3, MATRIX_0:24;
A9: dom (1. (K,(len bw1))) = Seg (len (1. (K,(len bw1)))) by FINSEQ_1:def 3;
A10: dom (1. (K,(len b1))) = Seg (len (1. (K,(len b1)))) by FINSEQ_1:def 3;
set BI = (len bw1) + i;
A11: ( dom bw2 = Seg (len bw2) & len (1. (K,(len bw2))) = len bw2 ) by FINSEQ_1:def 3, MATRIX_0:24;
set F2 = Mx2Tran (M2,bw2,Bu2);
A12: width (1. (K,(len b1))) = len b1 by MATRIX_0:24;
A13: ( len (Line (M2,i)) = width M2 & len ((width M1) |-> (0. K)) = width M1 ) by CARD_1:def 7;
A14: ( dom bw1 = Seg (len bw1) & len (1. (K,(len bw1))) = len bw1 ) by FINSEQ_1:def 3, MATRIX_0:24;
A15: len M = len b1 by MATRIX_0:def 2;
A16: len M1 = len bw1 by MATRIX_0:def 2;
then A17: dom M1 = dom bw1 by FINSEQ_3:29;
thus ( i in dom bw1 implies (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) ) :: thesis: ( i in dom bw2 implies (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) )

proof

A18: ( len (Line (M1,i)) = width M1 & len ((width M2) |-> (0. K)) = width M2 ) by CARD_1:def 7;
assume A19: i in dom bw1 ; :: thesis: (Mx2Tran (M,b1,B2)) . (b1 /. i) = (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i)
then A20: Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> (0. K)) by A3, A17, MATRIXJ1:23;
thus (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 A6, A19, MATRLIN2:19
.= Sum (lmlt ((Line ((LineVec2Mx (Line (((1. (K,(len b1))) * M),i))),1)),B2)) by A6, A8, A15, A10, A19, MATRIX_0:24, MATRLIN2:35
.= Sum (lmlt ((Line ((LineVec2Mx (Line (M,i))),1)),B2)) by A15, MATRIXR2:68
.= Sum (lmlt ((Line (M,i)),B2)) by MATRIX15:25
.= Sum ((lmlt ((Line (M1,i)),bu1)) ^ (lmlt (((width M2) |-> (0. K)),bu2))) by A2, A4, A5, A20, A18, MATRLIN2:9
.= (Sum (lmlt ((Line (M1,i)),bu1))) + (Sum (lmlt (((width M2) |-> (0. K)),bu2))) by RLVECT_1:41
.= (Sum (lmlt ((Line (M1,i)),bu1))) + ((0. K) * (Sum bu2)) by A5, MATRLIN2:11
.= (Sum (lmlt ((Line (M1,i)),bu1))) + (0. V2) by VECTSP_1:14
.= Sum (lmlt ((Line (M1,i)),bu1)) by RLVECT_1:def 4
.= Sum (lmlt ((Line (M1,i)),Bu1)) by MATRLIN2:14, MATRLIN2:15
.= Sum (lmlt ((Line ((LineVec2Mx (Line (M1,i))),1)),Bu1)) by MATRIX15:25
.= Sum (lmlt ((Line ((LineVec2Mx (Line (((1. (K,(len bw1))) * M1),i))),1)),Bu1)) by A16, MATRIXR2:68
.= Sum (lmlt ((Line (((LineVec2Mx (Line ((1. (K,(len bw1))),i))) * M1),1)),Bu1)) by A14, A9, A16, A19, MATRIX_0:24, MATRLIN2:35
.= Sum (lmlt ((Line (((LineVec2Mx ((bw1 /. i) |-- bw1)) * M1),1)),Bu1)) by A19, MATRLIN2:19
.= (Mx2Tran (M1,bw1,Bu1)) . (bw1 /. i) by MATRLIN2:def 3 ; :: thesis: verum

end;

A21: dom (1. (K,(len bw2))) = Seg (len (1. (K,(len bw2)))) by FINSEQ_1:def 3;
assume A22: i in dom bw2 ; :: thesis: (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i)
then A23: (len bw1) + i in dom b1 by A1, FINSEQ_1:28;
A24: len M2 = len bw2 by MATRIX_0:def 2;
then dom M2 = dom bw2 by FINSEQ_3:29;
then A25: Line (M,((len bw1) + i)) = ((width M1) |-> (0. K)) ^ (Line (M2,i)) by A3, A16, A22, MATRIXJ1:23;
thus (Mx2Tran (M,b1,B2)) . (b1 /. (i + (len bw1))) = Sum (lmlt ((Line (((LineVec2Mx ((b1 /. ((len bw1) + i)) |-- b1)) * M),1)),B2)) by MATRLIN2:def 3
.= Sum (lmlt ((Line (((LineVec2Mx (Line ((1. (K,(len b1))),((len bw1) + i)))) * M),1)),B2)) by A23, MATRLIN2:19
.= Sum (lmlt ((Line ((LineVec2Mx (Line (((1. (K,(len b1))) * M),((len bw1) + i)))),1)),B2)) by A1, A12, A8, A15, A10, A22, FINSEQ_1:28, MATRLIN2:35
.= Sum (lmlt ((Line ((LineVec2Mx (Line (M,((len bw1) + i)))),1)),B2)) by A15, MATRIXR2:68
.= Sum (lmlt ((Line (M,((len bw1) + i))),B2)) by MATRIX15:25
.= Sum ((lmlt (((width M1) |-> (0. K)),bu1)) ^ (lmlt ((Line (M2,i)),bu2))) by A2, A4, A5, A25, A13, MATRLIN2:9
.= (Sum (lmlt (((width M1) |-> (0. K)),bu1))) + (Sum (lmlt ((Line (M2,i)),bu2))) by RLVECT_1:41
.= ((0. K) * (Sum bu1)) + (Sum (lmlt ((Line (M2,i)),bu2))) by A4, MATRLIN2:11
.= (0. V2) + (Sum (lmlt ((Line (M2,i)),bu2))) by VECTSP_1:14
.= Sum (lmlt ((Line (M2,i)),bu2)) by RLVECT_1:def 4
.= Sum (lmlt ((Line (M2,i)),Bu2)) by MATRLIN2:14, MATRLIN2:15
.= Sum (lmlt ((Line ((LineVec2Mx (Line (M2,i))),1)),Bu2)) by MATRIX15:25
.= Sum (lmlt ((Line ((LineVec2Mx (Line (((1. (K,(len bw2))) * M2),i))),1)),Bu2)) by A24, MATRIXR2:68
.= Sum (lmlt ((Line (((LineVec2Mx (Line ((1. (K,(len bw2))),i))) * M2),1)),Bu2)) by A11, A21, A24, A22, MATRIX_0:24, MATRLIN2:35
.= Sum (lmlt ((Line (((LineVec2Mx ((bw2 /. i) |-- bw2)) * M2),1)),Bu2)) by A22, MATRLIN2:19
.= (Mx2Tran (M2,bw2,Bu2)) . (bw2 /. i) by MATRLIN2:def 3 ; :: thesis: verum