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) )
assume A1: for k being Element of NAT st k in dom p & k > n holds
p . k = 0. L ; :: thesis: Sum p = Sum (p | n)
defpred S₁[ Element of 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);
A2: S₁[ 0 ] by FINSEQ_1:79;

A3: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now

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 A5: ( len p = k + 1 & ( for l being Element of NAT st l in dom p & l > n holds
p . l = 0. L ) ) ; :: thesis: Sum p = Sum (p | n)
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence of L by FINSEQ_1:23;
A6: dom p = Seg (k + 1) by A5, FINSEQ_1:def 3;
A7: k <= len p by A5, NAT_1:11;
then A8: len q = k by FINSEQ_1:21;
A9: k <= k + 1 by NAT_1:11;
dom q = Seg k by A7, FINSEQ_1:21;
then A10: dom q c= dom p by A6, A9, FINSEQ_1:7;
A11: q ^ <*(p /. (k + 1))*> = q ^ <*(p . (k + 1))*> by A6, FINSEQ_1:6, PARTFUN1:def 8
.= p by A5, FINSEQ_3:61 ;
A12: q = p | k by FINSEQ_1:def 15;

now

per cases ( k < n or n <= k ) ;

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

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

A15: now

let u be set ; :: thesis: ( u in dom (p | n) implies u in dom p )
assume u in dom (p | n) ; :: thesis: u in dom p
then A16: u in dom (p | (Seg n)) by FINSEQ_1:def 15;
dom (p | (Seg n)) c= dom p by RELAT_1:89;
hence u in dom p by A16; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in dom p implies u in dom (p | n) )
assume A17: u in dom p ; :: thesis: u in dom (p | n)
then A18: u in Seg (k + 1) by A5, FINSEQ_1:def 3;
reconsider u' = u as Element of NAT by A17;
( 1 <= u' & u' <= k + 1 ) by A18, FINSEQ_1:3;
then ( 1 <= u' & u' <= n ) by A13, XXREAL_0:2;
then u' in Seg n by FINSEQ_1:3;
then u' in (dom p) /\ (Seg n) by A17, XBOOLE_0:def 4;
hence u in dom (p | n) by A14, RELAT_1:90; :: thesis: verum

end;

then A19: dom (p | n) = dom p by A15, TARSKI:2;
for x being set st x in dom (p | (Seg n)) holds
(p | (Seg n)) . x = p . x by FUNCT_1:70;
then p | (Seg n) = p by A14, A19, FUNCT_1:9;
hence Sum (p | n) = Sum p by FINSEQ_1:def 15; :: thesis: verum

end;

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

A21: now

let l be Element of NAT ; :: thesis: ( l in dom q & l > n implies q . l = 0. L )
assume A22: ( l in dom q & l > n ) ; :: thesis: q . l = 0. L
then A23: p . l = 0. L by A5, A10;
thus q . l = q /. l by A22, PARTFUN1:def 8
.= p /. l by A12, A22, FINSEQ_4:85
.= 0. L by A10, A22, A23, PARTFUN1:def 8 ; :: thesis: verum

end;

k + 1 > n by A20, NAT_1:13;
then A24: 0. L = p . (k + 1) by A5, A6, FINSEQ_1:6
.= p /. (k + 1) by A6, FINSEQ_1:6, PARTFUN1:def 8 ;
thus Sum p = (Sum q) + (Sum <*(p /. (k + 1))*>) by A11, RLVECT_1:58
.= (Sum q) + (p /. (k + 1)) by RLVECT_1:61
.= Sum q by A24, RLVECT_1:def 7
.= Sum (q | n) by A4, A8, A21
.= Sum (p | n) by A12, A20, FINSEQ_1:103 ; :: thesis: verum

end;

end;

end;

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

end;

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

end;

A25: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
consider k being Element of NAT such that
A26: len p = k ;
thus Sum p = Sum (p | n) by A1, A25, A26; :: thesis: verum