let i, j be Nat; :: thesis: for K being Field holds block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))
let K be Field; :: thesis: block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))
set I = 1. (K,i);
set J = 1. (K,j);
set B = block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K));
A1: len (1. (K,i)) = i by MATRIX_0:24;
A2: Sum (Len <*(1. (K,j))*>) = len (1. (K,j)) by Lm4;
A3: len (1. (K,j)) = j by MATRIX_0:24;
then A4: Indices (block_diagonal (<*(1. (K,j))*>,(0. K))) = [:(Seg j),(Seg j):] by A2, MATRIX_0:24;
Sum (Len <*(1. (K,i)),(1. (K,j))*>) = (len (1. (K,i))) + (len (1. (K,j))) by Th16;
then reconsider B = block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) as Matrix of i + j,K by A1, A3;
A5: Indices B = [:(Seg (i + j)),(Seg (i + j)):] by MATRIX_0:24;
A6: Indices (1. (K,j)) = [:(Seg j),(Seg j):] by MATRIX_0:24;
A7: width (1. (K,i)) = i by MATRIX_0:24;
A8: Indices (1. (K,i)) = [:(Seg i),(Seg i):] by MATRIX_0:24;
A9: Sum (Width <*(1. (K,i))*>) = width (1. (K,i)) by Lm5;
A10: Sum (Len <*(1. (K,i))*>) = len (1. (K,i)) by Lm4;
then A11: Indices (block_diagonal (<*(1. (K,i))*>,(0. K))) = [:(Seg i),(Seg i):] by A1, MATRIX_0:24;

A12: now :: thesis: for n, m being Nat st [n,m] in Indices B & n <> m holds
B * (n,m) = 0. K

let n, m be Nat; :: thesis: ( [n,m] in Indices B & n <> m implies B * (n,m) = 0. K )
assume that
A13: [n,m] in Indices B and
A14: n <> m ; :: thesis: B * (n,m) = 0. K
m in Seg (i + j) by A5, A13, ZFMISC_1:87;
then A15: m >= 1 by FINSEQ_1:1;
n in Seg (i + j) by A5, A13, ZFMISC_1:87;
then A16: n >= 1 by FINSEQ_1:1;

now :: thesis: B * (n,m) = 0. K

per cases ( ( n <= i & m <= i ) or ( n > i & m > i ) or ( n <= i & m > i ) or ( n > i & m <= i ) ) ;

suppose A17: ( n <= i & m <= i ) ; :: thesis: B * (n,m) = 0. K

then A18: m in Seg i by A15;
n in Seg i by A16, A17;
then A19: [n,m] in [:(Seg i),(Seg i):] by A18, ZFMISC_1:87;
hence B * (n,m) = (block_diagonal (<*(1. (K,i))*>,(0. K))) * (n,m) by A2, A11, Th26
.= (1. (K,i)) * (n,m) by Th34
.= 0. K by A8, A14, A19, MATRIX_1:def 3 ;
:: thesis: verum

end;

suppose A20: ( n > i & m > i ) ; :: thesis: B * (n,m) = 0. K

then A21: m - i <> 0 ;
n -' i = n - i by A20, XREAL_1:233;
then A22: n = (n -' i) + i ;
m -' i = m - i by A20, XREAL_1:233;
then A23: m = (m -' i) + i ;
n - i <> 0 by A20;
then A24: [(n -' i),(m -' i)] in [:(Seg j),(Seg j):] by A10, A9, A1, A7, A4, A13, A21, A22, A23, Th27;
hence B * (n,m) = (block_diagonal (<*(1. (K,j))*>,(0. K))) * ((n -' i),(m -' i)) by A10, A9, A1, A7, A4, A22, A23, Th28
.= (1. (K,j)) * ((n -' i),(m -' i)) by Th34
.= 0. K by A6, A14, A22, A23, A24, MATRIX_1:def 3 ;
:: thesis: verum

end;

suppose ( ( n <= i & m > i ) or ( n > i & m <= i ) ) ; :: thesis: B * (n,m) = 0. K

hence B * (n,m) = 0. K by A10, A9, A2, A1, A7, A13, Th29; :: thesis: verum

end;

end;

end;

hence B * (n,m) = 0. K ; :: thesis: verum

end;

now :: thesis: for n being Nat st [n,n] in Indices B holds
B * (n,n) = 1_ K

let n be Nat; :: thesis: ( [n,n] in Indices B implies B * (n,n) = 1_ K )
assume A25: [n,n] in Indices B ; :: thesis: B * (n,n) = 1_ K
n in Seg (i + j) by A5, A25, ZFMISC_1:87;
then A26: n >= 1 by FINSEQ_1:1;

now :: thesis: B * (n,n) = 1_ K

per cases ( n <= i or n > i ) ;

suppose n <= i ; :: thesis: B * (n,n) = 1_ K

then n in Seg i by A26;
then A27: [n,n] in [:(Seg i),(Seg i):] by ZFMISC_1:87;
hence B * (n,n) = (block_diagonal (<*(1. (K,i))*>,(0. K))) * (n,n) by A2, A11, Th26
.= (1. (K,i)) * (n,n) by Th34
.= 1_ K by A8, A27, MATRIX_1:def 3 ;
:: thesis: verum

end;

suppose A28: n > i ; :: thesis: B * (n,n) = 1_ K

then n -' i = n - i by XREAL_1:233;
then A29: n = (n -' i) + i ;
n - i <> 0 by A28;
then A30: [(n -' i),(n -' i)] in [:(Seg j),(Seg j):] by A10, A9, A1, A7, A4, A25, A29, Th27;
hence B * (n,n) = (block_diagonal (<*(1. (K,j))*>,(0. K))) * ((n -' i),(n -' i)) by A10, A9, A1, A7, A4, A29, Th28
.= (1. (K,j)) * ((n -' i),(n -' i)) by Th34
.= 1_ K by A6, A30, MATRIX_1:def 3 ;
:: thesis: verum

end;

end;

end;

hence B * (n,n) = 1_ K ; :: thesis: verum

end;

hence block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j)) by A12, MATRIX_1:def 3; :: thesis: verum