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

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

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

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

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

then p . (j + 1) = p /. (j + 1) by A1, PARTFUN1:def 6;
then fp . (j + 1) = (0. L) + (p /. (j + 1)) by A5, A10, A11, A12
.= p /. (j + 1) by ALGSTR_1:def 2 ;
hence S₁[j + 1] by A13; :: thesis: verum

end;

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

A15: j + 1 < i

proof

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

end;

j + 1 <= i by A12, NAT_1:13;
then A16: j + 1 <= l by A8, XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:6;
then A17: j + 1 in Seg l by A16, FINSEQ_1:1;
then p . (j + 1) = p /. (j + 1) by A6, PARTFUN1:def 6;
then fp . (j + 1) = (0. L) + (p /. (j + 1)) by A5, A10, A11, A12
.= p /. (j + 1) by ALGSTR_1:def 2
.= 0. L by A2, A6, A14, A17 ;
hence S₁[j + 1] by A15; :: thesis: verum

end;

end;

end;

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

j < l by A6, A10, FINSEQ_1:def 3;
then A19: j + 1 <= l by NAT_1:13;
A20: i < j + 1 by A18, NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:6;
then A21: j + 1 in dom p by A6, A19, FINSEQ_1:1;
then p . (j + 1) = p /. (j + 1) by PARTFUN1:def 6;
then fp . (j + 1) = (p /. i) + (p /. (j + 1)) by A5, A10, A11, A18
.= (p /. i) + (0. L) by A2, A20, A21
.= p /. i by RLVECT_1:def 4 ;
hence S₁[j + 1] by A18, NAT_1:13; :: thesis: verum

end;

end;

end;

A22: S₁[ 0 ] by A4, A8;
for j being Element of NAT st 0 <= j & j <= len p holds
S₁[j] from INT_1:sch 7(A22, A9);
hence Sum p = p /. i by A3, A8, A7; :: thesis: verum