let K be Field; :: thesis: for x being FinSequence of K
for a being Element of K st ex i being Element of NAT st
( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds
x . j = 0. K ) ) holds
Sum x = a
let x be FinSequence of K; :: thesis: for a being Element of K st ex i being Element of NAT st
( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds
x . j = 0. K ) ) holds
Sum x = a
let a be Element of K; :: thesis: ( ex i being Element of NAT st
( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds
x . j = 0. K ) ) implies Sum x = a )
given i being Element of NAT such that A1: 1 <= i and
A2: i <= len x and
A3: x . i = a and
A4: for j being Element of NAT st j <> i & 1 <= j & j <= len x holds
x . j = 0. K ; :: thesis: Sum x = a
1 <= len x by A1, A2, XXREAL_0:2;
then consider f being sequence of the carrier of K such that
A5: f . 1 = x . 1 and
A6: for n being Nat st 0 <> n & n < len x holds
f . (n + 1) = the addF of K . ((f . n),(x . (n + 1))) and
A7: the addF of K "**" x = f . (len x) by FINSOP_1:def 1;
A8: for j being Nat st 1 <= j & j < i holds
f . j = 0. K

proof

defpred S₁[ Nat] means ( 1 <= $1 & $1 < i implies f . $1 = 0. K );
let j be Nat; :: thesis: ( 1 <= j & j < i implies f . j = 0. K )
assume A9: ( 1 <= j & j < i ) ; :: thesis: f . j = 0. K
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( not 1 <= k or not k < i or ( 1 <= k & k < i ) ) ;

suppose A12: ( not 1 <= k or not k < i ) ; :: thesis: S₁[k + 1]

now :: thesis: S₁[k + 1]

per cases ( 1 > k or k >= i ) by A12;

suppose A13: 1 > k ; :: thesis: S₁[k + 1]

A14: 1 <= 1 + k by NAT_1:12;
1 >= k + 1 by A13, NAT_1:13;
then A15: k + 1 = 1 by A14, XXREAL_0:1;

now :: thesis: S₁[k + 1]

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

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

then k + 1 < len x by A2, XXREAL_0:2;
hence S₁[k + 1] by A4, A5, A15; :: thesis: verum

end;

suppose k + 1 >= i ; :: thesis: S₁[k + 1]

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

end;

end;

end;

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

end;

suppose k >= i ; :: thesis: S₁[k + 1]

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

end;

end;

end;

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

end;

suppose A16: ( 1 <= k & k < i ) ; :: thesis: S₁[k + 1]

then A17: k + 1 <= i by NAT_1:13;
A18: k < len x by A2, A16, XXREAL_0:2;

now :: thesis: S₁[k + 1]

per cases ( k + 1 < i or k + 1 = i ) by A17, XXREAL_0:1;

suppose A19: k + 1 < i ; :: thesis: S₁[k + 1]

then A20: k + 1 < len x by A2, XXREAL_0:2;
f . (k + 1) = the addF of K . ((f . k),(x . (k + 1))) by A6, A16, A18
.= (0. K) + (0. K) by A4, A11, A16, A19, A20, NAT_1:12
.= 0. K by RLVECT_1:4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;

end;

A21: S₁[ 0 ] ;
for l being Nat holds S₁[l] from NAT_1:sch 2(A21, A10);
hence f . j = 0. K by A9; :: thesis: verum

end;

for j being Element of NAT st i <= j & j <= len x holds
f . j = a

proof

defpred S₁[ Nat] means ( i <= $1 & $1 <= len x implies f . $1 = a );
let j be Element of NAT ; :: thesis: ( i <= j & j <= len x implies f . j = a )
assume A22: ( i <= j & j <= len x ) ; :: thesis: f . j = a
A23: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A24: S₁[k] ; :: thesis: S₁[k + 1]

per cases ( not i <= k + 1 or not k + 1 <= len x or ( i <= k + 1 & k + 1 <= len x ) ) ;

suppose ( not i <= k + 1 or not k + 1 <= len x ) ; :: thesis: S₁[k + 1]

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

end;

suppose A25: ( i <= k + 1 & k + 1 <= len x ) ; :: thesis: S₁[k + 1]

then A26: k < len x by NAT_1:13;
A27: 1 <= k + 1 by A1, A25, XXREAL_0:2;

now :: thesis: S₁[k + 1]

per cases ( i < k + 1 or i = k + 1 ) by A25, XXREAL_0:1;

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

A29: k < len x by A25, NAT_1:13;
i <= k by A28, NAT_1:13;
then f . (k + 1) = the addF of K . ((f . k),(x . (k + 1))) by A1, A6, A29
.= a + (0. K) by A4, A24, A25, A27, A28, NAT_1:13
.= a by RLVECT_1:4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

suppose A30: i = k + 1 ; :: thesis: S₁[k + 1]

then A31: k < i by NAT_1:13;

now :: thesis: S₁[k + 1]

per cases ( 1 <= k or k < 1 ) ;

suppose A32: 1 <= k ; :: thesis: S₁[k + 1]

then f . (k + 1) = the addF of K . ((f . k),(x . (k + 1))) by A6, A26
.= (0. K) + a by A3, A8, A30, A31, A32
.= a by RLVECT_1:4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

suppose k < 1 ; :: thesis: S₁[k + 1]

then A33: k + 1 <= 1 by NAT_1:13;
1 <= 1 + k by NAT_1:12;
then i = 1 by A30, A33, XXREAL_0:1;
hence S₁[k + 1] by A3, A5, A33, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

A34: S₁[ 0 ] by A1;
for l being Nat holds S₁[l] from NAT_1:sch 2(A34, A23);
hence f . j = a by A22; :: thesis: verum

end;

then f . (len x) = a by A2;
hence Sum x = a by A7, FVSUM_1:def 8; :: thesis: verum