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_1:24;
A2: Sum (Len <*(1. (K,j))*>) = len (1. (K,j)) by Lm4;
A3: len (1. (K,j)) = j by MATRIX_1:24;
then A4: Indices (block_diagonal (<*(1. (K,j))*>,(0. K))) = [:(Seg j),(Seg j):] by A2, MATRIX_1: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_1:24;
A6: Indices (1. (K,j)) = [:(Seg j),(Seg j):] by MATRIX_1:24;
A7: width (1. (K,i)) = i by MATRIX_1:24;
A8: Indices (1. (K,i)) = [:(Seg i),(Seg i):] by MATRIX_1: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_1:24;

A12: now

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
A15: m in Seg (i + j) by A5, A13, ZFMISC_1:87;
then A16: m >= 1 by FINSEQ_1:1;
A17: n in Seg (i + j) by A5, A13, ZFMISC_1:87;
then A18: n >= 1 by FINSEQ_1:1;

now

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

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

then A20: m in Seg i by A15, A16;
n in Seg i by A17, A18, A19;
then A21: [n,m] in [:(Seg i),(Seg i):] by A20, 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, A21, MATRIX_1:def 11 ;
:: thesis: verum

end;

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

then A23: m - i <> 0 ;
n -' i = n - i by A22, XREAL_1:233;
then A24: n = (n -' i) + i ;
m -' i = m - i by A22, XREAL_1:233;
then A25: m = (m -' i) + i ;
n - i <> 0 by A22;
then A26: [(n -' i),(m -' i)] in [:(Seg j),(Seg j):] by A10, A9, A1, A7, A4, A13, A23, A24, A25, Th27;
hence B * (n,m) = (block_diagonal (<*(1. (K,j))*>,(0. K))) * ((n -' i),(m -' i)) by A10, A9, A1, A7, A4, A24, A25, Th28
.= (1. (K,j)) * ((n -' i),(m -' i)) by Th34
.= 0. K by A6, A14, A24, A25, A26, MATRIX_1:def 11 ;
:: 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

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

now

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

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

then n in Seg i by A28, A29;
then A30: [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, A30, MATRIX_1:def 11 ;
:: thesis: verum

end;

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

then n -' i = n - i by XREAL_1:233;
then A32: n = (n -' i) + i ;
n - i <> 0 by A31;
then A33: [(n -' i),(n -' i)] in [:(Seg j),(Seg j):] by A10, A9, A1, A7, A4, A27, A32, Th27;
hence B * (n,n) = (block_diagonal (<*(1. (K,j))*>,(0. K))) * ((n -' i),(n -' i)) by A10, A9, A1, A7, A4, A32, Th28
.= (1. (K,j)) * ((n -' i),(n -' i)) by Th34
.= 1_ K by A6, A33, MATRIX_1:def 11 ;
:: 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 11; :: thesis: verum