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 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:
S1[ 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 A2:
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 (Len (1. K,f)) = len (1. K,f) &
len (1. K,f) = 0 )
by A2, FINSEQ_1:def 18, FINSEQ_3:31;
then
(
Len (1. K,f) = {} &
f = {} )
by A2;
then
(
Sum (Len (1. K,f)) = 0 &
Sum f = 0 )
by RVSUM_1:102;
hence
block_diagonal (1. K,f),
(0. K) = 1. K,
(Sum f)
by MATRIX_1:36;
:: thesis: verum
end;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
:: thesis: S1[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 A5:
len f = n + 1
;
:: thesis: block_diagonal (1. K,f),(0. K) = 1. K,(Sum f)
A6:
len (f | n) = n
by A5, FINSEQ_1:80, NAT_1:11;
1
<= n + 1
by NAT_1:11;
then
n + 1
in dom f
by A5, FINSEQ_3:27;
then AA:
f /. (n + 1) = f . (n + 1)
by PARTFUN1:def 8;
A7:
f = (f | n) ^ <*(f . (n + 1))*>
by A5, 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 Th58, AA
.=
block_diagonal ((1. K,(f | n)) ^ <*(1. K,(f . (n + 1)))*>),
(0. K)
by Th57, AA
.=
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 A4, A6
.=
1. K,
((Sum (f | n)) + (f . (n + 1)))
by Th60
.=
1. K,
(Sum f)
by A7, RVSUM_1:104
;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
then
S1[ len f]
;
hence
block_diagonal (1. K,f),(0. K) = 1. K,(Sum f)
; :: thesis: verum