let V be RealUnitarySpace; :: thesis: for u being Point of V
for n being Nat
for x being FinSequence of V st 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n)
let u be Point of V; :: thesis: for n being Nat
for x being FinSequence of V st 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n)
let n be Nat; :: thesis: for x being FinSequence of V st 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n)
defpred S₁[ Nat] means for x being FinSequence of V st $1 = len x & 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n);
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let x be FinSequence of V; :: thesis: ( k + 1 = len x & 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) implies u .|. (Sum x) = u .|. (x /. n) )
assume A4: ( k + 1 = len x & 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) ) ; :: thesis: u .|. (Sum x) = u .|. (x /. n)
then A5: n in dom x by FINSEQ_3:25;
defpred S₂[ Nat, object ] means $2 = u .|. (x /. $1);
A6: for k being Nat st k in Seg (len x) holds
ex v being Element of REAL st S₂[k,v] ;
consider r being FinSequence of REAL such that
A7: ( dom r = Seg (len x) & ( for k being Nat st k in Seg (len x) holds
S₂[k,r . k] ) ) from FINSEQ_1:sch 5(A6);
A8: ( len x = len r & ( for i being Nat st 1 <= i & i <= len x holds
r . i = u .|. (x /. i) ) ) by A7, FINSEQ_1:def 3, FINSEQ_1:1;
set x1 = x | k;
set r1 = r | k;
A11: ( len (x | k) = k & len (r | k) = k ) by A4, A8, FINSEQ_1:59, NAT_1:11;
A24: dom (r | k) = Seg (len (r | k)) by FINSEQ_1:def 3;

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

suppose A25: n = k + 1 ; :: thesis: u .|. (Sum x) = u .|. (x /. n)

for i being object st i in dom (r | k) holds
(r | k) . i = 0

proof

let t be object ; :: thesis: ( t in dom (r | k) implies (r | k) . t = 0 )
assume A27: t in dom (r | k) ; :: thesis: (r | k) . t = 0
then reconsider i = t as Nat ;
A28: ( 1 <= i & i <= len (r | k) ) by A27, A24, FINSEQ_1:1;
A29: i <= k by A11, A27, A24, FINSEQ_1:1;
then A31: i <= len x by A4, NAT_1:13;
i <> n by NAT_1:13, A25, A29;
then u .|. (x /. i) = 0 by A4, A28, A31;
then r . i = 0 by A28, A31, A7, FINSEQ_1:1;
hence (r | k) . t = 0 by A27, A24, FUNCT_1:49, A11; :: thesis: verum

end;

then r | k = (len (r | k)) |-> 0 by FINSEQ_1:def 3;
then A32: Sum (r | k) = 0 by RVSUM_1:81;
r = (r | k) ^ <*(r . (k + 1))*> by FINSEQ_3:55, A8, A4
.= (r | k) ^ <*(u .|. (x /. n))*> by A25, A4, A7, FINSEQ_1:1 ;
then W1: Sum r = 0 + (u .|. (x /. n)) by A32, RVSUM_1:74;
u .|. (Sum x) = Sum (u .|. x) by Th4;
hence u .|. (Sum x) = u .|. (x /. n) by A8, W1, DefSK; :: thesis: verum

end;

suppose A33: n <> k + 1 ; :: thesis: u .|. (Sum x) = u .|. (x /. n)

A34: ( k = len (x | k) & 1 <= n & n <= len (x | k) & ( for i being Nat st 1 <= i & i <= len (x | k) & n <> i holds
u .|. ((x | k) /. i) = 0 ) )

proof

n < k + 1 by A33, A4, XXREAL_0:1;
hence ( k = len (x | k) & 1 <= n & n <= len (x | k) ) by NAT_1:13, A4, A11; :: thesis: for i being Nat st 1 <= i & i <= len (x | k) & n <> i holds
u .|. ((x | k) /. i) = 0
let i be Nat; :: thesis: ( 1 <= i & i <= len (x | k) & n <> i implies u .|. ((x | k) /. i) = 0 )
assume A35: ( 1 <= i & i <= len (x | k) & n <> i ) ; :: thesis: u .|. ((x | k) /. i) = 0
k <= k + 1 by NAT_1:11;
then A36: i <= len x by A4, A11, A35, XXREAL_0:2;
A38: i in Seg k by A35, A11;
A39: i in dom (x | k) by A35, FINSEQ_3:25;
i in dom x by A35, A36, FINSEQ_3:25;
then x /. i = x . i by PARTFUN1:def 6
.= (x | k) . i by FUNCT_1:49, A38
.= (x | k) /. i by PARTFUN1:def 6, A39 ;
hence u .|. ((x | k) /. i) = 0 by A4, A35, A36; :: thesis: verum

end;

then A40: n in Seg k ;
then n in dom (x | k) by A11, FINSEQ_1:def 3;
then A41: (x | k) /. n = (x | k) . n by PARTFUN1:def 6
.= x . n by FUNCT_1:49, A40
.= x /. n by PARTFUN1:def 6, A5 ;
A43: len x = (len (x | k)) + 1 by A4, FINSEQ_1:59, NAT_1:11;
A44: dom (x | k) = Seg k by A11, FINSEQ_1:def 3;
A0: 1 <= k + 1 by NAT_1:11;
then k + 1 in dom x by A4, FINSEQ_3:25;
then A45a: x /. (k + 1) = x . (len x) by A4, PARTFUN1:def 6;
A46: u .|. (x /. (k + 1)) = 0 by A33, A4, A0;
thus u .|. (Sum x) = u .|. ((Sum (x | k)) + (x /. (k + 1))) by A45a, A43, A44, RLVECT_1:38
.= (u .|. (Sum (x | k))) + (u .|. (x /. (k + 1))) by BHSP_1:2
.= u .|. (x /. n) by A46, A41, A3, A34 ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence for x being FinSequence of V st 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n) ; :: thesis: verum