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₁[ 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 S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[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 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 16;
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) ) )

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 16;
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)

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;

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 16;
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 A14, TARSKI:2;
then p | (Seg n) = p by A12, A18, FUNCT_1:2;
hence Sum (p | n) = Sum p by FINSEQ_1:def 16; :: 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 A22, PARTFUN1:def 6
.= p /. l by A9, A22, FINSEQ_4:70
.= 0. L by A8, A22, A24, PARTFUN1:def 6 ; :: thesis: verum

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

end;

end;

end;

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

end;

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

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: Sum p = Sum (p | n)
hence Sum p = Sum (p | n) by A27, A28; :: thesis: verum