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 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 :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
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)
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 ;
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence of L by FINSEQ_1:18;
A6: k <= len p by ;
then A7: len q = k by FINSEQ_1:17;
( k <= k + 1 & dom q = Seg k ) by ;
then A8: dom q c= dom p by ;
A9: q = p | k by FINSEQ_1:def 15;
A10: q ^ <*(p /. (k + 1))*> = q ^ <*(p . (k + 1))*> by
.= p by ;
now :: thesis: ( ( k < n & Sum (p | n) = Sum p ) or ( n <= k & Sum p = Sum (p | n) ) )
per cases ( k < n or n <= k ) ;
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 ;
A14: now :: thesis: for u being object st u in dom p 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 ;
then u9 <= k + 1 by FINSEQ_1:1;
then A17: u9 <= n by ;
1 <= u9 by ;
then u9 in Seg n by ;
then u9 in (dom p) /\ (Seg n) by ;
hence u in dom (p | n) by ; :: thesis: verum
end;
A18: for x being object st x in dom (p | (Seg n)) holds
(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
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;
then dom (p | n) = dom p by ;
then p | (Seg n) = p by ;
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 :: thesis: for l being Element of NAT st l in dom q & l > n holds
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
.= p /. l by
.= 0. L by ; :: thesis: verum
end;
k + 1 > n by ;
then A25: 0. L = p . (k + 1) by
.= p /. (k + 1) by ;
thus Sum p = (Sum q) + (Sum <*(p /. (k + 1))*>) by
.= (Sum q) + (p /. (k + 1)) by RLVECT_1:44
.= Sum q by
.= Sum (q | n) by A2, A7, A21
.= Sum (p | n) by ; :: thesis: verum
end;
end;
end;
hence Sum p = Sum (p | n) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: 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 ; :: thesis: Sum p = Sum (p | n)
hence Sum p = Sum (p | n) by ; :: thesis: verum