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

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

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

now

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

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

then p . (j + 1) = p /. (j + 1) by A1, PARTFUN1:def 8;
then fp . (j + 1) = (0. L) + (p /. (j + 1)) by A2, A7, A8, A9
.= p /. (j + 1) by ALGSTR_1:def 5 ;
hence S₁[j + 1] by A10; :: thesis: verum

end;

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

j + 1 <= i by A9, NAT_1:13;
then A12: j + 1 <= l by A4, XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:8;
then A13: j + 1 in Seg l by A12, FINSEQ_1:3;
then p . (j + 1) = p /. (j + 1) by A3, PARTFUN1:def 8;
then A14: fp . (j + 1) = (0. L) + (p /. (j + 1)) by A2, A7, A8, A9
.= p /. (j + 1) by ALGSTR_1:def 5
.= 0. L by A1, A3, A11, A13 ;
j + 1 < i

proof

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

end;

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

end;

end;

end;

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

end;

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

then A16: i < j + 1 by NAT_1:13;
j < l by A3, A7, FINSEQ_1:def 3;
then A17: j + 1 <= l by NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:8;
then A18: j + 1 in dom p by A3, A17, FINSEQ_1:3;
then p . (j + 1) = p /. (j + 1) by PARTFUN1:def 8;
then fp . (j + 1) = (p /. i) + (p /. (j + 1)) by A2, A7, A8, A15
.= (p /. i) + (0. L) by A1, A16, A18
.= p /. i by RLVECT_1:def 7 ;
hence S₁[j + 1] by A15, NAT_1:13; :: thesis: verum

end;

end;

end;

A19: for j being Element of NAT st 0 <= j & j <= len p holds
S₁[j] from POLYNOM2:sch 4(A5, A6);
len p = l by A3, FINSEQ_1:def 3;
hence Sum p = p /. i by A2, A4, A19; :: thesis: verum