let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for F, G being FinSequence of V st len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) holds
Sum F = - (Sum G)
let F, G be FinSequence of V; :: thesis: ( len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) implies Sum F = - (Sum G) )
defpred S₁[ set ] means for H, I being FinSequence of V st len H = len I & len H = $1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I);
A1: dom F = Seg (len F) by FINSEQ_1:def 3;

now :: thesis: for n being Nat st ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ) holds
for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)

let n be Nat; :: thesis: ( ( for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ) implies for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) )
assume A2: for H, I being FinSequence of V st len H = len I & len H = n & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I) ; :: thesis: for H, I being FinSequence of V st len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)
let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) implies Sum H = - (Sum I) )
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ; :: thesis: Sum H = - (Sum I)
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of the carrier of V by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then A7: len q = n by A3, A4, FINSEQ_1:17;
A8: len p = n by A4, A6, FINSEQ_1:17;

A9: now :: thesis: for k being Nat
for v being Element of V st k in Seg (len p) & v = q . k holds
p . k = - v

len p <= len H by A4, A6, FINSEQ_1:17;
then A10: Seg (len p) c= Seg (len H) by FINSEQ_1:5;
A11: dom p = Seg n by A4, A6, FINSEQ_1:17;
let k be Nat; :: thesis: for v being Element of V st k in Seg (len p) & v = q . k holds
p . k = - v
let v be Element of V; :: thesis: ( k in Seg (len p) & v = q . k implies p . k = - v )
assume that
A12: k in Seg (len p) and
A13: v = q . k ; :: thesis: p . k = - v
dom q = Seg n by A3, A4, A6, FINSEQ_1:17;
then I . k = q . k by A8, A12, FUNCT_1:47;
then H . k = - v by A5, A12, A13, A10;
hence p . k = - v by A8, A12, A11, FUNCT_1:47; :: thesis: verum

end;

1 <= n + 1 by NAT_1:11;
then ( n + 1 in dom H & n + 1 in dom I ) by A3, A4, FINSEQ_3:25;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as Element of V by FUNCT_1:102;
A14: v1 = - v2 by A4, A5, FINSEQ_1:4;
A15: dom q = Seg (len q) by FINSEQ_1:def 3;
dom p = Seg (len p) by FINSEQ_1:def 3;
hence Sum H = (Sum p) + v1 by A4, A8, Th38
.= (- (Sum q)) + (- v2) by A2, A8, A7, A9, A14
.= - ((Sum q) + v2) by Lm3
.= - (Sum I) by A3, A4, A7, A15, Th38 ;
:: thesis: verum

end;

then A16: for n being Nat st S₁[n] holds
S₁[n + 1] ;

now :: thesis: for H, I being FinSequence of V st len H = len I & len H = 0 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) holds
Sum H = - (Sum I)

let H, I be FinSequence of V; :: thesis: ( len H = len I & len H = 0 & ( for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ) implies Sum H = - (Sum I) )
assume that
A17: ( len H = len I & len H = 0 ) and
for k being Nat
for v being Element of V st k in Seg (len H) & v = I . k holds
H . k = - v ; :: thesis: Sum H = - (Sum I)
( Sum H = 0. V & Sum I = 0. V ) by A17, Lm5;
hence Sum H = - (Sum I) ; :: thesis: verum

end;

then A18: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A18, A16);
hence ( len F = len G & ( for k being Nat
for v being Element of V st k in dom F & v = G . k holds
F . k = - v ) implies Sum F = - (Sum G) ) by A1; :: thesis: verum