let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for F1, F2 being FinSequence of L st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 /. i = - (F2 /. i) ) holds
Sum F1 = - (Sum F2)
let F1, F2 be FinSequence of L; :: thesis: ( len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 /. i = - (F2 /. i) ) implies Sum F1 = - (Sum F2) )
assume that
A1: len F1 = len F2 and
A2: for i being Element of NAT st i in dom F1 holds
F1 /. i = - (F2 /. i) ; :: thesis: Sum F1 = - (Sum F2)
defpred S₁[ Nat] means for F1, F2 being FinSequence of L st len F1 = $1 & len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 /. i = - (F2 /. i) ) holds
Sum F1 = - (Sum F2);

A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f, g being FinSequence of L st len f = k + 1 & len f = len g & ( for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ) holds
Sum f = - (Sum g)

let f, g be FinSequence of L; :: thesis: ( len f = k + 1 & len f = len g & ( for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ) implies Sum f = - (Sum g) )
assume that
A5: len f = k + 1 and
A6: len f = len g and
A7: for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ; :: thesis: Sum f = - (Sum g)
set f1 = f | (Seg k);
set g1 = g | (Seg k);
reconsider f1 = f | (Seg k), g1 = g | (Seg k) as FinSequence by FINSEQ_1:15;
reconsider f1 = f1, g1 = g1 as FinSequence of L by A5, A6, Lm1;
A8: len f1 = k by A5, Lm1;
A9: len g1 = k by A5, A6, Lm1;
then A10: dom f1 = Seg (len g1) by A8, FINSEQ_1:def 3
.= dom g1 by FINSEQ_1:def 3 ;
A11: f = f1 ^ <*(f /. (k + 1))*> by A5, Lm1;
A12: g = g1 ^ <*(g /. (k + 1))*> by A5, A6, Lm1;

A13: now :: thesis: for i being Element of NAT st i in dom f1 holds
f1 /. i = - (g1 /. i)

A14: dom f1 c= dom f by A5, Lm1;
let i be Element of NAT ; :: thesis: ( i in dom f1 implies f1 /. i = - (g1 /. i) )
assume A15: i in dom f1 ; :: thesis: f1 /. i = - (g1 /. i)
dom g1 c= dom g by A5, A6, Lm1;
then A16: g /. i = g . i by A10, A15, PARTFUN1:def 6
.= g1 . i by A12, A10, A15, FINSEQ_1:def 7
.= g1 /. i by A10, A15, PARTFUN1:def 6 ;
thus f1 /. i = f1 . i by A15, PARTFUN1:def 6
.= f . i by A11, A15, FINSEQ_1:def 7
.= f /. i by A15, A14, PARTFUN1:def 6
.= - (g1 /. i) by A7, A15, A14, A16 ; :: thesis: verum

end;

1 <= k + 1 by NAT_1:11;
then A17: k + 1 in dom f by A5, FINSEQ_3:25;
thus Sum f = (Sum f1) + (Sum <*(f /. (k + 1))*>) by A11, RLVECT_1:41
.= (- (Sum g1)) + (Sum <*(f /. (k + 1))*>) by A4, A8, A9, A13
.= (- (Sum g1)) + (f /. (k + 1)) by RLVECT_1:44
.= (- (Sum g1)) + (- (g /. (k + 1))) by A7, A17
.= - ((Sum g1) + (g /. (k + 1))) by RLVECT_1:31
.= - ((Sum g1) + (Sum <*(g /. (k + 1))*>)) by RLVECT_1:44
.= - (Sum g) by A12, RLVECT_1:41 ; :: thesis: verum

end;

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

end;

now :: thesis: for f, g being FinSequence of L st len f = 0 & len f = len g & ( for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ) holds
Sum f = - (Sum g)

let f, g be FinSequence of L; :: thesis: ( len f = 0 & len f = len g & ( for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ) implies Sum f = - (Sum g) )
assume that
A18: len f = 0 and
A19: len f = len g and
for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ; :: thesis: Sum f = - (Sum g)
A20: g = <*> the carrier of L by A18, A19;
f = <*> the carrier of L by A18;
hence Sum f = 0. L by RLVECT_1:43
.= - (0. L) by RLVECT_1:12
.= - (Sum g) by A20, RLVECT_1:43 ;
:: thesis: verum

end;

then A21: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A3);
hence Sum F1 = - (Sum F2) by A1, A2; :: thesis: verum