let L be non empty right_complementable add-associative right_zeroed addLoopStr ; for p being FinSequence of L
for n being Element of NAT st ( for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ) holds
Sum p = Sum (p | n)
let p be FinSequence of L; for n being Element of NAT st ( for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ) holds
Sum p = Sum (p | n)
let n be Element of NAT ; ( ( for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ) implies Sum p = Sum (p | n) )
defpred S1[ Nat] means for p being FinSequence of L
for n being Element of NAT st len p = $1 & ( for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ) holds
Sum p = Sum (p | n);
A1:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A2:
S1[
k]
;
S1[k + 1]now for p being FinSequence of L
for n being Element of NAT st len p = k + 1 & ( for l being Element of NAT st l in dom p & l > n holds
p . l = 0. L ) holds
Sum p = Sum (p | n)let p be
FinSequence of
L;
for n being Element of NAT st len p = k + 1 & ( for l being Element of NAT st l in dom p & l > n holds
p . l = 0. L ) holds
Sum p = Sum (p | n)let n be
Element of
NAT ;
( len p = k + 1 & ( for l being Element of NAT st l in dom p & l > n holds
p . l = 0. L ) implies Sum p = Sum (p | n) )assume that A3:
len p = k + 1
and A4:
for
l being
Element of
NAT st
l in dom p &
l > n holds
p . l = 0. L
;
Sum p = Sum (p | n)A5:
dom p = Seg (k + 1)
by A3, FINSEQ_1:def 3;
set q =
p | (Seg k);
reconsider q =
p | (Seg k) as
FinSequence of
L by FINSEQ_1:18;
A6:
k <= len p
by A3, NAT_1:11;
then A7:
len q = k
by FINSEQ_1:17;
(
k <= k + 1 &
dom q = Seg k )
by A6, FINSEQ_1:17, NAT_1:11;
then A8:
dom q c= dom p
by A5, FINSEQ_1:5;
A9:
q = p | k
by FINSEQ_1:def 15;
A10:
q ^ <*(p /. (k + 1))*> =
q ^ <*(p . (k + 1))*>
by A5, FINSEQ_1:4, PARTFUN1:def 6
.=
p
by A3, FINSEQ_3:55
;
now ( ( k < n & Sum (p | n) = Sum p ) or ( n <= k & Sum p = Sum (p | n) ) )per cases
( k < n or n <= k )
;
case A20:
n <= k
;
Sum p = Sum (p | n)
k + 1
> n
by A20, NAT_1:13;
then A25:
0. L =
p . (k + 1)
by A4, A5, FINSEQ_1:4
.=
p /. (k + 1)
by A5, FINSEQ_1:4, PARTFUN1:def 6
;
thus Sum p =
(Sum q) + (Sum <*(p /. (k + 1))*>)
by A10, RLVECT_1:41
.=
(Sum q) + (p /. (k + 1))
by RLVECT_1:44
.=
Sum q
by A25, RLVECT_1:def 4
.=
Sum (q | n)
by A2, A7, A21
.=
Sum (p | n)
by A9, A20, FINSEQ_1:82
;
verum end; end; end; hence
Sum p = Sum (p | n)
;
verum end; hence
S1[
k + 1]
;
verum end;
A26:
S1[ 0 ]
by FINSEQ_1:58;
A27:
for k being Nat holds S1[k]
from NAT_1:sch 2(A26, A1);
A28:
ex k being Element of NAT st len p = k
;
assume
for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L
; Sum p = Sum (p | n)
hence
Sum p = Sum (p | n)
by A27, A28; verum