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:59, NAT_1:11;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom f by A3, FINSEQ_3:25;
then A5: f /. (n + 1) = f . (n + 1) by PARTFUN1:def 6;
A6: f = (f | n) ^ <*(f . (n + 1))*> by A3, FINSEQ_3:55;
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:74 ;
:: 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:29;
then A9: Sum (Len (1. (K,f))) = 0 by RVSUM_1:72;
f = {} by A8;
hence block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f)) by A9, MATRIX_0:45, RVSUM_1:72; :: 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