let L be non empty Abelian add-associative addLoopStr ; :: thesis: for a being Element of L
for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) holds
Sum q = a + (Sum p)
let a be Element of L; :: thesis: for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) holds
Sum q = a + (Sum p)
let p, q be FinSequence of the carrier of L; :: thesis: ( len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) implies Sum q = a + (Sum p) )
assume that
A1: len p = len q and
A2: ex i being Element of NAT st
( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) ; :: thesis: Sum q = a + (Sum p)
consider i being Element of NAT such that
A3: i in dom p and
A4: q /. i = a + (p /. i) and
A5: for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 by A2;
consider fq being sequence of the carrier of L such that
A6: Sum q = fq . (len q) and
A7: fq . 0 = 0. L and
A8: for j being Nat
for v being Element of L st j < len q & v = q . (j + 1) holds
fq . (j + 1) = (fq . j) + v by RLVECT_1:def 12;
consider l being Nat such that
A9: dom p = Seg l by FINSEQ_1:def 2;
i in { z where z is Nat : ( 1 <= z & z <= l ) } by A3, A9, FINSEQ_1:def 1;
then A10: ex i9 being Nat st
( i9 = i & 1 <= i9 & i9 <= l ) ;
consider l9 being Nat such that
A11: dom q = Seg l9 by FINSEQ_1:def 2;
reconsider l = l, l9 = l9 as Element of NAT by ORDINAL1:def 12;
consider fp being sequence of the carrier of L such that
A12: Sum p = fp . (len p) and
A13: fp . 0 = 0. L and
A14: for j being Nat
for v being Element of L st j < len p & v = p . (j + 1) holds
fp . (j + 1) = (fp . j) + v by RLVECT_1:def 12;
A15: len p = l by A9, FINSEQ_1:def 3;
defpred S₁[ Element of NAT ] means ( ( $1 < i & fp . $1 = fq . $1 ) or ( i <= $1 & fq . $1 = a + (fp . $1) ) );
A16: l = len p by A9, FINSEQ_1:def 3
.= l9 by A1, A11, FINSEQ_1:def 3 ;
A17: for j being Element of NAT st 0 <= j & j < len p & S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len p & S₁[j] implies S₁[j + 1] )
assume that
0 <= j and
A18: j < len p ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A19: S₁[j] ; :: thesis: S₁[j + 1]

per cases ( j < i or i <= j ) ;

suppose A20: j < i ; :: thesis: S₁[j + 1]

per cases ( j + 1 = i or j + 1 <> i ) ;

suppose A21: j + 1 = i ; :: thesis: S₁[j + 1]

then A22: p . (j + 1) = p /. (j + 1) by A3, PARTFUN1:def 6;
q . (j + 1) = q /. (j + 1) by A3, A9, A11, A16, A21, PARTFUN1:def 6;
then fq . (j + 1) = (fq . j) + (a + (p /. (j + 1))) by A1, A4, A8, A18, A21
.= a + ((fq . j) + (p /. (j + 1))) by RLVECT_1:def 3
.= a + (fp . (j + 1)) by A14, A18, A19, A20, A22 ;
hence S₁[j + 1] by A21; :: thesis: verum

end;

suppose A23: j + 1 <> i ; :: thesis: S₁[j + 1]

A24: j + 1 < i

proof

assume i <= j + 1 ; :: thesis: contradiction
then i < j + 1 by A23, XXREAL_0:1;
hence contradiction by A20, NAT_1:13; :: thesis: verum

end;

j + 1 <= i by A20, NAT_1:13;
then A25: j + 1 <= l by A10, XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:6;
then A26: j + 1 in Seg l by A25, FINSEQ_1:1;
then A27: p . (j + 1) = p /. (j + 1) by A9, PARTFUN1:def 6;
q . (j + 1) = q /. (j + 1) by A11, A16, A26, PARTFUN1:def 6;
then fq . (j + 1) = (fq . j) + (q /. (j + 1)) by A1, A8, A18
.= fp . (j + 1) by A5, A14, A9, A18, A19, A20, A23, A26, A27 ;
hence S₁[j + 1] by A24; :: thesis: verum

end;

end;

end;

suppose A28: i <= j ; :: thesis: S₁[j + 1]

j < l by A9, A18, FINSEQ_1:def 3;
then A29: j + 1 <= l by NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:6;
then A30: j + 1 in dom p by A9, A29, FINSEQ_1:1;
then A31: p . (j + 1) = p /. (j + 1) by PARTFUN1:def 6;
A32: i < j + 1 by A28, NAT_1:13;
q . (j + 1) = q /. (j + 1) by A9, A11, A16, A30, PARTFUN1:def 6;
then fq . (j + 1) = (fq . j) + (q /. (j + 1)) by A1, A8, A18
.= (a + (fp . j)) + (p /. (j + 1)) by A5, A19, A28, A32, A30
.= a + ((fp . j) + (p /. (j + 1))) by RLVECT_1:def 3
.= a + (fp . (j + 1)) by A14, A18, A31 ;
hence S₁[j + 1] by A28, NAT_1:13; :: thesis: verum

end;

end;

end;

A33: S₁[ 0 ] by A13, A7, A10;
for j being Element of NAT st 0 <= j & j <= len p holds
S₁[j] from INT_1:sch 7(A33, A17);
hence Sum q = a + (Sum p) by A1, A12, A6, A10, A15; :: thesis: verum