let K be Field; for f being FinSequence of NAT holds block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f))
let f be FinSequence of NAT ; block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f))
defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let f be
FinSequence of
NAT ;
( len f = n + 1 implies block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f)) )
assume A3:
len f = n + 1
;
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
;
verum
end;
A7:
S1[ 0 ]
proof
let f be
FinSequence of
NAT ;
( len f = 0 implies block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f)) )
assume A8:
len f = 0
;
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;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A1);
then
S1[ len f]
;
hence
block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f))
; verum