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 i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) 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 i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) 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 i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) implies Sum q = a + (Sum p) )
assume A1: ( len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a + (p /. i) & ( for i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) ) ; :: thesis: Sum q = a + (Sum p)
then consider i being Element of NAT such that
A2: ( i in dom p & q /. i = a + (p /. i) & ( for i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) ;
consider fp being Function of NAT ,the carrier of L such that
A3: ( Sum p = fp . (len p) & fp . 0 = 0. L & ( for j being Element of 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 13;
consider fq being Function of NAT ,the carrier of L such that
A4: ( Sum q = fq . (len q) & fq . 0 = 0. L & ( for j being Element of 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 13;
defpred S₁[ Element of NAT ] means ( ( $1 < i & fp . $1 = fq . $1 ) or ( i <= $1 & fq . $1 = a + (fp . $1) ) );
consider l being Nat such that
A5: dom p = Seg l by FINSEQ_1:def 2;
i in { z where z is Element of NAT : ( 1 <= z & z <= l ) } by A2, A5, FINSEQ_1:def 1;
then consider i' being Element of NAT such that
A6: ( i' = i & 1 <= i' & i' <= l ) ;
consider l' being Nat such that
A7: dom q = Seg l' by FINSEQ_1:def 2;
reconsider l = l, l' = l' as Element of NAT by ORDINAL1:def 13;
A8: l = len p by A5, FINSEQ_1:def 3
.= l' by A1, A7, FINSEQ_1:def 3 ;
A9: S₁[ 0 ] by A3, A4, A6;
A10: 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 A11: ( 0 <= j & j < len p ) ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A12: S₁[j] ; :: thesis: S₁[j + 1]

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

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

now

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

case A14: j + 1 = i ; :: thesis: S₁[j + 1]

then A15: p . (j + 1) = p /. (j + 1) by A2, PARTFUN1:def 8;
q . (j + 1) = q /. (j + 1) by A2, A5, A7, A8, A14, PARTFUN1:def 8;
then fq . (j + 1) = (fq . j) + (a + (p /. (j + 1))) by A1, A2, A4, A11, A14
.= a + ((fq . j) + (p /. (j + 1))) by RLVECT_1:def 6
.= a + (fp . (j + 1)) by A3, A11, A12, A13, A15 ;
hence S₁[j + 1] by A14; :: thesis: verum

end;

case A16: j + 1 <> i ; :: thesis: S₁[j + 1]

j + 1 <= i by A13, NAT_1:13;
then A17: j + 1 <= l by A6, XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:8;
then A18: j + 1 in Seg l by A17, FINSEQ_1:3;
then A19: p . (j + 1) = p /. (j + 1) by A5, PARTFUN1:def 8;
q . (j + 1) = q /. (j + 1) by A7, A8, A18, PARTFUN1:def 8;
then A20: fq . (j + 1) = (fq . j) + (q /. (j + 1)) by A1, A4, A11
.= fp . (j + 1) by A2, A3, A5, A11, A12, A13, A16, A18, A19 ;
j + 1 < i

proof

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

end;

hence S₁[j + 1] by A20; :: thesis: verum

end;

end;

end;

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

end;

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

then A22: i < j + 1 by NAT_1:13;
j < l by A5, A11, FINSEQ_1:def 3;
then A23: j + 1 <= l by NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:8;
then A24: j + 1 in dom p by A5, A23, FINSEQ_1:3;
then A25: p . (j + 1) = p /. (j + 1) by PARTFUN1:def 8;
q . (j + 1) = q /. (j + 1) by A5, A7, A8, A24, PARTFUN1:def 8;
then fq . (j + 1) = (fq . j) + (q /. (j + 1)) by A1, A4, A11
.= (a + (fp . j)) + (p /. (j + 1)) by A2, A12, A21, A22, A24
.= a + ((fp . j) + (p /. (j + 1))) by RLVECT_1:def 6
.= a + (fp . (j + 1)) by A3, A11, A25 ;
hence S₁[j + 1] by A21, NAT_1:13; :: thesis: verum

end;

end;

end;

A26: for j being Element of NAT st 0 <= j & j <= len p holds
S₁[j] from POLYNOM2:sch 4(A9, A10);
len p = l by A5, FINSEQ_1:def 3;
hence Sum q = a + (Sum p) by A1, A3, A4, A6, A26; :: thesis: verum