let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( ( 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 S_{1}[ 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);

_{1}[ 0 ]
by FINSEQ_1:58;

A27: for k being Nat holds S_{1}[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 ; :: thesis: Sum p = Sum (p | n)

hence Sum p = Sum (p | n) by A27, A28; :: thesis: verum

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; :: thesis: 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 ; :: thesis: ( ( 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 S

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 :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A26:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A2: S

now :: thesis: 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)

hence
Sfor 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ;

end;p . l = 0. L ) holds

Sum p = Sum (p | n)

let n be Element of NAT ; :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( ( k < n & Sum (p | n) = Sum p ) or ( n <= k & Sum p = Sum (p | n) ) )end;

hence
Sum p = Sum (p | n)
; :: thesis: verumper cases
( k < n or n <= k )
;

end;

case A11:
k < n
; :: thesis: Sum (p | n) = Sum p

A12:
dom (p | n) = dom (p | (Seg n))
by FINSEQ_1:def 15;

A13: k + 1 <= n by A11, NAT_1:13;

(p | (Seg n)) . x = p . x by FUNCT_1:47;

then p | (Seg n) = p by A12, A18, FUNCT_1:2;

hence Sum (p | n) = Sum p by FINSEQ_1:def 15; :: thesis: verum

end;A13: k + 1 <= n by A11, NAT_1:13;

A14: now :: thesis: for u being object st u in dom p holds

u in dom (p | n)

A18:
for x being object st x in dom (p | (Seg n)) holds u in dom (p | n)

let u be object ; :: thesis: ( u in dom p implies u in dom (p | n) )

assume A15: u in dom p ; :: thesis: u in dom (p | n)

then reconsider u9 = u as Element of NAT ;

A16: u in Seg (k + 1) by A3, A15, FINSEQ_1:def 3;

then u9 <= k + 1 by FINSEQ_1:1;

then A17: u9 <= n by A13, XXREAL_0:2;

1 <= u9 by A16, FINSEQ_1:1;

then u9 in Seg n by A17, FINSEQ_1:1;

then u9 in (dom p) /\ (Seg n) by A15, XBOOLE_0:def 4;

hence u in dom (p | n) by A12, RELAT_1:61; :: thesis: verum

end;assume A15: u in dom p ; :: thesis: u in dom (p | n)

then reconsider u9 = u as Element of NAT ;

A16: u in Seg (k + 1) by A3, A15, FINSEQ_1:def 3;

then u9 <= k + 1 by FINSEQ_1:1;

then A17: u9 <= n by A13, XXREAL_0:2;

1 <= u9 by A16, FINSEQ_1:1;

then u9 in Seg n by A17, FINSEQ_1:1;

then u9 in (dom p) /\ (Seg n) by A15, XBOOLE_0:def 4;

hence u in dom (p | n) by A12, RELAT_1:61; :: thesis: verum

(p | (Seg n)) . x = p . x by FUNCT_1:47;

now :: thesis: for u being object st u in dom (p | n) holds

u in dom p

then
dom (p | n) = dom p
by A14, TARSKI:2;u in dom p

let u be object ; :: thesis: ( u in dom (p | n) implies u in dom p )

assume u in dom (p | n) ; :: thesis: u in dom p

then A19: u in dom (p | (Seg n)) by FINSEQ_1:def 15;

dom (p | (Seg n)) c= dom p by RELAT_1:60;

hence u in dom p by A19; :: thesis: verum

end;assume u in dom (p | n) ; :: thesis: u in dom p

then A19: u in dom (p | (Seg n)) by FINSEQ_1:def 15;

dom (p | (Seg n)) c= dom p by RELAT_1:60;

hence u in dom p by A19; :: thesis: verum

then p | (Seg n) = p by A12, A18, FUNCT_1:2;

hence Sum (p | n) = Sum p by FINSEQ_1:def 15; :: thesis: verum

case A20:
n <= k
; :: thesis: Sum p = Sum (p | n)

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 ; :: thesis: verum

end;

A21: now :: thesis: for l being Element of NAT st l in dom q & l > n holds

q . l = 0. L

k + 1 > n
by A20, NAT_1:13;q . l = 0. L

let l be Element of NAT ; :: thesis: ( l in dom q & l > n implies q . l = 0. L )

assume that

A22: l in dom q and

A23: l > n ; :: thesis: q . l = 0. L

A24: p . l = 0. L by A4, A8, A22, A23;

thus q . l = q /. l by A22, PARTFUN1:def 6

.= p /. l by A9, A22, FINSEQ_4:70

.= 0. L by A8, A22, A24, PARTFUN1:def 6 ; :: thesis: verum

end;assume that

A22: l in dom q and

A23: l > n ; :: thesis: q . l = 0. L

A24: p . l = 0. L by A4, A8, A22, A23;

thus q . l = q /. l by A22, PARTFUN1:def 6

.= p /. l by A9, A22, FINSEQ_4:70

.= 0. L by A8, A22, A24, PARTFUN1:def 6 ; :: thesis: verum

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 ; :: thesis: verum

A27: for k being Nat holds S

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 ; :: thesis: Sum p = Sum (p | n)

hence Sum p = Sum (p | n) by A27, A28; :: thesis: verum