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 A1: ( len F1 = len F2 & ( 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);

now

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 ( len f = 0 & len f = len g & ( for i being Element of NAT st i in dom f holds
f /. i = - (g /. i) ) ) ; :: thesis: Sum f = - (Sum g)
then A2: ( f = <*> the carrier of L & g = <*> the carrier of L ) by FINSEQ_1:32;
hence Sum f = 0. L by RLVECT_1:60
.= - (0. L) by RLVECT_1:25
.= - (Sum g) by A2, RLVECT_1:60 ;
:: thesis: verum

end;

then A3: S₁[ 0 ] ;

A4: now

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

now

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 A6: ( len f = k + 1 & len f = len g & ( 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:19;
reconsider f1 = f1, g1 = g1 as FinSequence of L by A6, Lm1;
A7: ( len f1 = k & len g1 = k ) by A6, Lm1;
A8: f = f1 ^ <*(f /. (k + 1))*> by A6, Lm1;
A9: g = g1 ^ <*(g /. (k + 1))*> by A6, Lm1;
A10: dom f1 = Seg (len g1) by A7, FINSEQ_1:def 3
.= dom g1 by FINSEQ_1:def 3 ;

A11: now

let i be Element of NAT ; :: thesis: ( i in dom f1 implies f1 /. i = - (g1 /. i) )
assume A12: i in dom f1 ; :: thesis: f1 /. i = - (g1 /. i)
A13: ( dom f1 c= dom f & dom g1 c= dom g ) by A6, Lm1;
then A14: g /. i = g . i by A10, A12, PARTFUN1:def 8
.= g1 . i by A9, A10, A12, FINSEQ_1:def 7
.= g1 /. i by A10, A12, PARTFUN1:def 8 ;
thus f1 /. i = f1 . i by A12, PARTFUN1:def 8
.= f . i by A8, A12, FINSEQ_1:def 7
.= f /. i by A12, A13, PARTFUN1:def 8
.= - (g1 /. i) by A6, A12, A13, A14 ; :: thesis: verum

end;

1 <= k + 1 by NAT_1:11;
then A15: k + 1 in dom f by A6, FINSEQ_3:27;
thus Sum f = (Sum f1) + (Sum <*(f /. (k + 1))*>) by A8, RLVECT_1:58
.= (- (Sum g1)) + (Sum <*(f /. (k + 1))*>) by A5, A7, A11
.= (- (Sum g1)) + (f /. (k + 1)) by RLVECT_1:61
.= (- (Sum g1)) + (- (g /. (k + 1))) by A6, A15
.= - ((Sum g1) + (g /. (k + 1))) by RLVECT_1:45
.= - ((Sum g1) + (Sum <*(g /. (k + 1))*>)) by RLVECT_1:61
.= - (Sum g) by A9, RLVECT_1:58 ; :: thesis: verum

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
hence Sum F1 = - (Sum F2) by A1; :: thesis: verum