let V be RealUnitarySpace; :: thesis: for u being Point of V
for x being FinSequence of V holds u .|. (Sum x) = Sum (u .|. x)
let u be Point of V; :: thesis: for x being FinSequence of V holds u .|. (Sum x) = Sum (u .|. x)
let x be FinSequence of V; :: thesis: u .|. (Sum x) = Sum (u .|. x)
defpred S₁[ Nat] means for x being FinSequence of V st $1 = len x holds
u .|. (Sum x) = Sum (u .|. x);
A1: S₁[ 0 ]

proof

let x be FinSequence of V; :: thesis: ( 0 = len x implies u .|. (Sum x) = Sum (u .|. x) )
assume A2: 0 = len x ; :: thesis: u .|. (Sum x) = Sum (u .|. x)
then x = <*> the carrier of V ;
then A3: Sum x = 0. V by RLVECT_1:43;
set r = u .|. x;
len (u .|. x) = len x by DefSK;
then u .|. x = <*> REAL by A2;
hence u .|. (Sum x) = Sum (u .|. x) by A3, BHSP_1:15, RVSUM_1:72; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let x be FinSequence of V; :: thesis: ( k + 1 = len x implies u .|. (Sum x) = Sum (u .|. x) )
set r = u .|. x;
set x1 = x | k;
set r1 = (u .|. x) | k;
assume A6: k + 1 = len x ; :: thesis: u .|. (Sum x) = Sum (u .|. x)
then A7: ( 1 <= k + 1 & k + 1 <= len x ) by NAT_1:11;
A8: k <= k + 1 by NAT_1:11;
B1: len (u .|. x) = len x by DefSK;
then A9: ( len (x | k) = k & len ((u .|. x) | k) = k ) by A6, FINSEQ_1:59, NAT_1:11;
for i being Nat st 1 <= i & i <= len (x | k) holds
((u .|. x) | k) . i = u .|. ((x | k) /. i)

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (x | k) implies ((u .|. x) | k) . i = u .|. ((x | k) /. i) )
assume A10: ( 1 <= i & i <= len (x | k) ) ; :: thesis: ((u .|. x) | k) . i = u .|. ((x | k) /. i)
then A11: i <= len x by A8, A9, A6, XXREAL_0:2;
then A13: i in dom x by A10, FINSEQ_3:25;
A20: ((u .|. x) | k) . i = (u .|. x) . i by FUNCT_1:49, A9, A10, FINSEQ_1:1;
i in dom (x | k) by A10, FINSEQ_3:25;
then (x | k) /. i = (x | k) . i by PARTFUN1:def 6
.= x . i by FUNCT_1:49, A9, A10, FINSEQ_1:1
.= x /. i by A13, PARTFUN1:def 6 ;
hence ((u .|. x) | k) . i = u .|. ((x | k) /. i) by A10, A20, A11, DefSK; :: thesis: verum

end;

then A22b: (u .|. x) | k = u .|. (x | k) by A9, DefSK;
A23a: u .|. x = ((u .|. x) | k) ^ <*((u .|. x) . (k + 1))*> by B1, FINSEQ_3:55, A6
.= ((u .|. x) | k) ^ <*(u .|. (x /. (k + 1)))*> by A7, DefSK ;
A24: len x = (len (x | k)) + 1 by A6, FINSEQ_1:59, NAT_1:11;
A25: dom (x | k) = Seg k by A9, FINSEQ_1:def 3;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom x by A6, FINSEQ_1:def 3;
then x /. (k + 1) = x . (len x) by A6, PARTFUN1:def 6;
hence u .|. (Sum x) = u .|. ((Sum (x | k)) + (x /. (k + 1))) by A24, A25, RLVECT_1:38
.= (u .|. (Sum (x | k))) + (u .|. (x /. (k + 1))) by BHSP_1:2
.= (Sum ((u .|. x) | k)) + (u .|. (x /. (k + 1))) by A22b, A5, A9
.= Sum (u .|. x) by A23a, RVSUM_1:74 ;
:: thesis: verum

end;

B3: len (u .|. x) = len x by DefSK;
for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
hence u .|. (Sum x) = Sum (u .|. x) by B3; :: thesis: verum