let K be Field; :: thesis: for f being FinSequence of NAT holds block_diagonal (1. K,f),(0. K) = 1. K,(Sum f)
let f be FinSequence of NAT ; :: thesis: block_diagonal (1. K,f),(0. K) = 1. K,(Sum f)
defpred S₁[ Nat] means for f being FinSequence of NAT st len f = $1 holds
block_diagonal (1. K,f),(0. K) = 1. K,(Sum f);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let f be FinSequence of NAT ; :: thesis: ( len f = n + 1 implies block_diagonal (1. K,f),(0. K) = 1. K,(Sum f) )
assume A3: len f = n + 1 ; :: thesis: block_diagonal (1. K,f),(0. K) = 1. K,(Sum f)
A4: len (f | n) = n by A3, FINSEQ_1:80, NAT_1:11;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom f by A3, FINSEQ_3:27;
then A5: f /. (n + 1) = f . (n + 1) by PARTFUN1:def 8;
A6: f = (f | n) ^ <*(f . (n + 1))*> by A3, FINSEQ_3:61;
hence block_diagonal (1. K,f),(0. K) = block_diagonal ((1. K,(f | n)) ^ (1. K,<*(f /. (n + 1))*>)),(0. K) by A5, Th58
.= block_diagonal ((1. K,(f | n)) ^ <*(1. K,(f . (n + 1)))*>),(0. K) by A5, Th57
.= block_diagonal (<*(block_diagonal (1. K,(f | n)),(0. K))*> ^ <*(1. K,(f . (n + 1)))*>),(0. K) by Th35
.= block_diagonal <*(1. K,(Sum (f | n))),(1. K,(f . (n + 1)))*>,(0. K) by A2, A4
.= 1. K,((Sum (f | n)) + (f . (n + 1))) by Th60
.= 1. K,(Sum f) by A6, RVSUM_1:104 ;
:: thesis: verum

end;

A7: S₁[ 0 ]

proof

let f be FinSequence of NAT ; :: thesis: ( len f = 0 implies block_diagonal (1. K,f),(0. K) = 1. K,(Sum f) )
assume A8: len f = 0 ; :: thesis: block_diagonal (1. K,f),(0. K) = 1. K,(Sum f)
dom (1. K,f) = dom f by Def8;
then len (1. K,f) = 0 by A8, FINSEQ_3:31;
then A9: Sum (Len (1. K,f)) = 0 by RVSUM_1:102;
f = {} by A8;
hence block_diagonal (1. K,f),(0. K) = 1. K,(Sum f) by A9, MATRIX_1:36, RVSUM_1:102; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A1);
then S₁[ len f] ;
hence block_diagonal (1. K,f),(0. K) = 1. K,(Sum f) ; :: thesis: verum