let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis:
let p be FinSequence of L; :: thesis:
let n be Element of NAT ; :: thesis:
defpred S₁[ 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 :: thesis:

let k be Nat; :: thesis:
assume A2: S₁[k] ; :: thesis:

let p be FinSequence of L; :: thesis:
let n be Element of NAT ; :: thesis:
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:
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 ;

case A11: k < n ; :: thesis:

A12: dom (p | n) = dom (p | (Seg n)) by FINSEQ_1:def 15;
A13: k + 1 <= n by A11, NAT_1:13;

A14: now :: thesis:

let u be object ; :: thesis:
assume A15: u in dom p ; :: thesis:
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:

end;

A18: for x being object st x in dom (p | (Seg n)) holds
(p | (Seg n)) . x = p . x by FUNCT_1:47;

let u be object ; :: thesis:
assume u in dom (p | n) ; :: thesis:
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:

end;

then dom (p | n) = dom p by A14, TARSKI:2;
then p | (Seg n) = p by A12, A18, FUNCT_1:2;
hence Sum (p | n) = Sum p by FINSEQ_1:def 15; :: thesis:

end;

case A20: n <= k ; :: thesis:

A21: now :: thesis:

let l be Element of NAT ; :: thesis:
assume that
A22: l in dom q and
A23: l > n ; :: thesis:
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:

end;

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

end;

end;

end;

hence Sum p = Sum (p | n) ; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A26: S₁[ 0 ] by FINSEQ_1:58;
A27: for k being Nat holds S₁[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:
hence Sum p = Sum (p | n) by A27, A28; :: thesis: