let n be Nat; :: thesis:
let F, F2 be FinSequence of REAL n; :: thesis:
let h be Permutation of (dom F); :: thesis:
assume A1: F2 = F (*) h ; :: thesis:

suppose A2: len F > 0 ; :: thesis:

then A3: 0 + 1 <= len F by NAT_1:13;
then A4: 1 in Seg (len F) by FINSEQ_1:1;
then A5: 1 in dom F by FINSEQ_1:def 3;
then A6: dom h = dom F by FUNCT_2:def 1;
then rng h = dom h by FUNCT_2:def 3;
then A7: dom F2 = dom h by A1, RELAT_1:27;
then A8: Seg (len F2) = dom F by A6, FINSEQ_1:def 3;
set gF = accum F;
A9: len F = len (accum F) by Def10;
A10: for i being Nat st 1 <= i & i < len F holds
(accum F) . (i + 1) = ((accum F) /. i) + (F /. (i + 1)) by Def10;
defpred S₁[ Nat] means for h2 being Permutation of (dom F) st $1 < len F & ( for i being Nat st $1 + 1 < i & i <= len F holds
h2 . i = i ) holds
(accum F) . ($1 + 1) = (accum (F (*) h2)) . ($1 + 1);
A11: dom F = Seg (len F) by FINSEQ_1:def 3;
1 in Seg (len F2) by A5, A6, A7, FINSEQ_1:def 3;
then A12: 1 <= len F2 by FINSEQ_1:1;
A13: (len F) -' 1 = (len F) - 1 by A3, XREAL_1:233;
then A14: for i being Nat st ((len F) -' 1) + 1 < i & i <= len F holds
h . i = i ;
A15: dom F <> {} by A4, FINSEQ_1:def 3;
A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A17: S₁[k] ; :: thesis:
for h2 being Permutation of (dom F) st k + 1 < len F & ( for i being Nat st (k + 1) + 1 < i & i <= len F holds
h2 . i = i ) holds
(accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1)

proof

A18: 1 <= k + 1 by NAT_1:11;
A19: k + 1 < (k + 1) + 1 by XREAL_1:29;
let h2 be Permutation of (dom F); :: thesis:
assume that
A20: k + 1 < len F and
A21: for i being Nat st (k + 1) + 1 < i & i <= len F holds
h2 . i = i ; :: thesis:
A22: (k + 1) + 1 <= len F by A20, NAT_1:13;
k < k + 1 by XREAL_1:29;
then A23: k < len F by A20, XXREAL_0:2;
A24: 1 < (k + 1) + 1 by XREAL_1:29;
then A25: (k + 1) + 1 in Seg (len F) by A22, FINSEQ_1:1;
then A26: (k + 1) + 1 in dom F by FINSEQ_1:def 3;
A27: dom h2 = dom F by A5, FUNCT_2:def 1;
then A28: rng h2 = dom h2 by FUNCT_2:def 3;
then A29: dom (F (*) h2) = dom h2 by RELAT_1:27
.= dom F by A5, FUNCT_2:def 1 ;
then A30: Seg (len (F (*) h2)) = dom F by FINSEQ_1:def 3;
then A31: Seg (len (F (*) h2)) = Seg (len F) by FINSEQ_1:def 3;
A32: len (F (*) h2) = len F by A30, FINSEQ_1:def 3;
h2 is FinSequence by A11, A27, FINSEQ_1:def 2;
then reconsider h2r = h2 as FinSequence of NAT by A27, A28, FINSEQ_1:def 4;
dom h2 = Seg (len F) by A2, A11, FUNCT_2:def 1;
then A33: len h2r = len F by FINSEQ_1:def 3;
consider x being object such that
A34: x in dom h2 and
A35: (k + 1) + 1 = h2 . x by A11, A27, A28, A25, FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A27, A34;
A36: nx <= len F by A11, A34, FINSEQ_1:1;
reconsider h2b = Swap (h2r,nx,((k + 1) + 1)) as FinSequence of NAT ;
A37: rng h2b = rng h2 by FINSEQ_7:22
.= dom F by FUNCT_2:def 3 ;
A38: len h2b = len h2r by FINSEQ_7:18;
then dom h2b = Seg (len h2r) by FINSEQ_1:def 3;
then A39: dom h2b = dom h2 by FINSEQ_1:def 3
.= dom F by A15, FUNCT_2:def 1 ;
then reconsider h2d = h2b as Function of (dom F),(dom F) by A37, FUNCT_2:1;
A40: h2d is one-to-one by INT_5:39;
h2d is onto by A37, FUNCT_2:def 3;
then reconsider h4 = h2d as Permutation of (dom F) by A40;
A41: 1 <= nx by A11, A34, FINSEQ_1:1;
then A42: h4 . nx = h2r . ((k + 1) + 1) by A22, A24, A36, A33, Th9;
A43: dom h4 = dom F by A5, FUNCT_2:def 1;
rng h4 c= dom F ;
then A44: dom (F (*) h4) = dom h4 by RELAT_1:27
.= dom F by A5, FUNCT_2:def 1 ;
then Seg (len (F (*) h4)) = dom F by FINSEQ_1:def 3;
then A45: len (F (*) h4) = len F by FINSEQ_1:def 3;

per cases ;

suppose A46: nx <= k + 1 ; :: thesis:

A47: (k + 1) + 1 <= len h2r by A20, A33, NAT_1:13;
A48: nx <= len h2r by A11, A34, A33, FINSEQ_1:1;
A49: F . ((k + 1) + 1) = (F (*) h2) . nx by A34, A35, FUNCT_1:13;
A50: len (accum (F (*) h4)) = len (F (*) h4) by Def10;
A51: 1 <= nx by A11, A34, FINSEQ_1:1;
A52: 1 <= (k + 1) + 1 by NAT_1:11;
then A53: h2b . ((k + 1) + 1) = (k + 1) + 1 by A35, A51, A48, A47, Th9;
A54: for i being Nat st k + 1 < i & i <= len F holds
h4 . i = i

proof

let i be Nat; :: thesis:
assume that
A55: k + 1 < i and
A56: i <= len F ; :: thesis:
A57: (k + 1) + 1 <= i by A55, NAT_1:13;

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

suppose A58: (k + 1) + 1 < i ; :: thesis:

1 <= k + 1 by NAT_1:11;
then A59: 1 < i by A55, XXREAL_0:2;
then h4 . i = h2b /. i by A33, A38, A56, FINSEQ_4:15
.= h2r /. i by A33, A46, A55, A56, A58, A59, FINSEQ_7:30
.= h2 . i by A33, A56, A59, FINSEQ_4:15
.= i by A21, A56, A58 ;
hence h4 . i = i ; :: thesis:

end;

suppose (k + 1) + 1 >= i ; :: thesis:

then i = (k + 1) + 1 by A57, XXREAL_0:1;
hence h4 . i = i by A35, A51, A48, A52, A47, Th9; :: thesis:

end;

A60: F /. ((k + 1) + 1) = F . ((k + 1) + 1) by A22, A24, FINSEQ_4:15;
A61: 1 <= k + 1 by NAT_1:11;
A62: len (accum (F (*) h2)) = len (F (*) h2) by Def10;
A63: nx < (k + 1) + 1 by A19, A46, XXREAL_0:2;
A64: for i4 being Nat st 1 <= i4 & i4 < nx holds
(accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4

proof

defpred S₂[ Nat] means ( 1 + $1 < nx implies (accum (F (*) h2)) . (1 + $1) = (accum (F (*) h4)) . (1 + $1) );
let i4 be Nat; :: thesis:
assume that
A65: 1 <= i4 and
A66: i4 < nx ; :: thesis:
A67: 1 + (i4 -' 1) = (i4 - 1) + 1 by A65, XREAL_1:233
.= i4 ;
A68: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

let k3 be Nat; :: thesis:
A69: 1 <= k3 + 1 by NAT_1:11;
assume A70: S₂[k3] ; :: thesis:
( 1 + (k3 + 1) < nx implies (accum (F (*) h2)) . (1 + (k3 + 1)) = (accum (F (*) h4)) . (1 + (k3 + 1)) )

proof

assume A71: 1 + (k3 + 1) < nx ; :: thesis:
then A72: 1 + (k3 + 1) < len F by A36, XXREAL_0:2;
then A73: h2r /. ((k3 + 1) + 1) = h2r . ((k3 + 1) + 1) by A33, FINSEQ_4:15, NAT_1:11;
A74: (k3 + 1) + 1 < (k + 1) + 1 by A63, A71, XXREAL_0:2;
A75: h2b /. ((k3 + 1) + 1) = h2b . ((k3 + 1) + 1) by A33, A38, A72, FINSEQ_4:15, NAT_1:11;
1 <= 1 + (k3 + 1) by NAT_1:11;
then (k3 + 1) + 1 in Seg (len F) by A72, FINSEQ_1:1;
then A76: (k3 + 1) + 1 in dom (F (*) h2) by A29, FINSEQ_1:def 3;
then A77: (F (*) h2) . ((k3 + 1) + 1) = F . (h2 . ((k3 + 1) + 1)) by FUNCT_1:12
.= F . (h4 . ((k3 + 1) + 1)) by A33, A71, A72, A74, A73, A75, FINSEQ_7:30, NAT_1:11
.= (F (*) h4) . ((k3 + 1) + 1) by A44, A29, A76, FUNCT_1:12 ;
A78: (F (*) h4) /. ((k3 + 1) + 1) = (F (*) h4) . ((k3 + 1) + 1) by A45, A72, FINSEQ_4:15, NAT_1:11;
A79: k3 + 1 < 1 + (k3 + 1) by XREAL_1:29;
then A80: k3 + 1 < nx by A71, XXREAL_0:2;
then A81: k3 + 1 < len F by A36, XXREAL_0:2;
k3 + 1 < len (F (*) h2) by A36, A32, A80, XXREAL_0:2;
then A82: (accum (F (*) h4)) /. (1 + k3) = (accum (F (*) h4)) . (1 + k3) by A45, A32, A50, FINSEQ_4:15, NAT_1:11;
(accum (F (*) h2)) /. (1 + k3) = (accum (F (*) h2)) . (1 + k3) by A32, A62, A81, FINSEQ_4:15, NAT_1:11;
then (accum (F (*) h2)) . (1 + (k3 + 1)) = ((accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h2) /. ((k3 + 1) + 1)) by A32, A70, A69, A71, A79, A81, A82, Def10, XXREAL_0:2
.= ((accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h4) /. ((k3 + 1) + 1)) by A32, A72, A77, A78, FINSEQ_4:15, NAT_1:11 ;
hence (accum (F (*) h2)) . (1 + (k3 + 1)) = (accum (F (*) h4)) . (1 + (k3 + 1)) by A45, A69, A81, Def10; :: thesis:

end;

hence S₂[k3 + 1] ; :: thesis:

end;

0 < k + 1 ;
then A83: 1 <> (k + 1) + 1 ;
A84: h2b /. 1 = h2b . 1 by A3, A33, A38, FINSEQ_4:15;
A85: h2r /. 1 = h2r . 1 by A3, A33, FINSEQ_4:15;
(F (*) h2) . 1 = F . (h2 . 1) by A5, A29, FUNCT_1:12
.= F . (h4 . 1) by A3, A33, A65, A66, A83, A85, A84, FINSEQ_7:30
.= (F (*) h4) . 1 by A5, A44, FUNCT_1:12 ;
then (accum (F (*) h2)) . (1 + 0) = (F (*) h4) . 1 by Def10
.= (accum (F (*) h4)) . (1 + 0) by Def10 ;
then A86: S₂[ 0 ] ;
for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A86, A68);
hence (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4 by A66, A67; :: thesis:

end;

A87: for i being Nat st nx <= i & i < (k + 1) + 1 holds
(accum (F (*) h2)) . i = (((accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)

proof

defpred S₂[ Nat] means ( nx <= nx + $1 & nx + $1 < (k + 1) + 1 implies (accum (F (*) h2)) . (nx + $1) = (((accum (F (*) h4)) /. (nx + $1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) );
let i be Nat; :: thesis:
assume that
A88: nx <= i and
A89: i < (k + 1) + 1 ; :: thesis:
A90: len (accum (F (*) h4)) = len (F (*) h4) by Def10;
A91: len (accum (F (*) h2)) = len (F (*) h2) by Def10;
A92: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

let k3 be Nat; :: thesis:
assume A93: S₂[k3] ; :: thesis:
( nx <= nx + (k3 + 1) & nx + (k3 + 1) < (k + 1) + 1 implies (accum (F (*) h2)) . (nx + (k3 + 1)) = (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) )

proof

reconsider f3 = (F (*) h2) /. ((nx + k3) + 1) as Element of REAL n ;
A94: nx <= nx + k3 by NAT_1:11;
reconsider f2 = (F (*) h2) /. ((k + 1) + 1) as Element of REAL n ;
A95: nx + k3 < (nx + k3) + 1 by XREAL_1:29;
reconsider f4 = (F (*) h2) /. nx as Element of REAL n ;
reconsider f1 = (accum (F (*) h4)) /. (nx + k3) as Element of REAL n ;
assume that
nx <= nx + (k3 + 1) and
A96: nx + (k3 + 1) < (k + 1) + 1 ; :: thesis:
A97: nx + (k3 + 1) < len (accum (F (*) h4)) by A22, A45, A90, A96, XXREAL_0:2;
A98: nx + k3 < (nx + k3) + 1 by XREAL_1:29;
then nx + k3 < (k + 1) + 1 by A96, XXREAL_0:2;
then A99: nx + k3 < len (F (*) h2) by A33, A32, A47, XXREAL_0:2;
then A100: (nx + k3) + 1 <= len (F (*) h2) by NAT_1:13;
nx + k3 >= 0 + 1 by A41, NAT_1:13;
then A101: 1 < nx + (k3 + 1) by A98, XXREAL_0:2;
then A102: (F (*) h4) /. ((nx + k3) + 1) = (F (*) h4) . ((nx + k3) + 1) by A45, A32, A100, FINSEQ_4:15;
(nx + k3) + 1 in Seg (len (F (*) h2)) by A101, A100, FINSEQ_1:1;
then A103: (nx + k3) + 1 in dom (F (*) h2) by FINSEQ_1:def 3;
then A104: (F (*) h4) . ((nx + k3) + 1) = F . (h4 . ((nx + k3) + 1)) by A44, A29, FUNCT_1:12
.= F . (h2b /. ((nx + k3) + 1)) by A33, A38, A32, A101, A100, FINSEQ_4:15
.= F . (h2r /. ((nx + k3) + 1)) by A33, A32, A96, A101, A100, A95, A94, FINSEQ_7:30
.= F . (h2r . ((nx + k3) + 1)) by A33, A32, A101, A100, FINSEQ_4:15
.= (F (*) h2) . ((nx + k3) + 1) by A103, FUNCT_1:12 ;
nx <= nx + k3 by NAT_1:11;
then A105: 1 <= nx + k3 by A51, XXREAL_0:2;
then (accum (F (*) h4)) . (nx + (k3 + 1)) = ((accum (F (*) h4)) /. (nx + k3)) + ((F (*) h4) /. ((nx + k3) + 1)) by A45, A32, A99, Def10
.= ((accum (F (*) h4)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1)) by A101, A100, A104, A102, FINSEQ_4:15 ;
then A106: (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) = ((f1 + f3) - f2) + f4 by A101, A97, FINSEQ_4:15
.= ((f1 - f2) + f3) + f4 by RFUNCT_1:8
.= ((f1 - f2) + f4) + f3 by RFUNCT_1:8 ;
(accum (F (*) h2)) . (nx + (k3 + 1)) = ((accum (F (*) h2)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1)) by A105, A99, Def10
.= ((((accum (F (*) h4)) /. (nx + k3)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((nx + k3) + 1)) by A91, A93, A96, A98, A105, A99, FINSEQ_4:15, NAT_1:11, XXREAL_0:2 ;
hence (accum (F (*) h2)) . (nx + (k3 + 1)) = (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A106; :: thesis:

end;

hence S₂[k3 + 1] ; :: thesis:

end;

now :: thesis:

per cases by A41, XXREAL_0:1;

case A107: 1 = nx ; :: thesis:

(accum (F (*) h4)) /. (nx + 0) = (accum (F (*) h4)) . 1 by A3, A45, A90, A107, FINSEQ_4:15
.= (F (*) h4) . 1 by Def10
.= F . (h2 . ((k + 1) + 1)) by A5, A43, A42, A107, FUNCT_1:13
.= (F (*) h2) . ((k + 1) + 1) by A27, A26, FUNCT_1:13
.= (F (*) h2) /. ((k + 1) + 1) by A22, A24, A32, FINSEQ_4:15 ;
then A108: (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) = (0* n) + ((F (*) h2) /. nx) by EUCLIDLP:2
.= (F (*) h2) /. nx by EUCLID_4:1 ;
(accum (F (*) h2)) . (nx + 0) = (F (*) h2) . 1 by A107, Def10
.= (F (*) h2) /. nx by A36, A32, A107, FINSEQ_4:15 ;
hence (accum (F (*) h2)) . (nx + 0) = (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A108; :: thesis:

end;

case A109: 1 < nx ; :: thesis:

A110: (F (*) h4) /. nx = (F (*) h4) . nx by A41, A36, A45, FINSEQ_4:15
.= F . (h2 . ((k + 1) + 1)) by A34, A43, A42, FUNCT_1:13
.= (F (*) h2) . ((k + 1) + 1) by A27, A26, FUNCT_1:13
.= (F (*) h2) /. ((k + 1) + 1) by A22, A24, A32, FINSEQ_4:15 ;
A111: nx -' 1 = nx - 1 by A109, XREAL_1:233;
then nx -' 1 > 0 by A109, XREAL_1:50;
then A112: nx -' 1 >= 0 + 1 by NAT_1:13;
nx < nx + 1 by XREAL_1:29;
then A113: nx - 1 < (nx + 1) - 1 by XREAL_1:9;
then A114: nx -' 1 < len (F (*) h2) by A33, A32, A48, A111, XXREAL_0:2;
then A115: (accum (F (*) h2)) /. (nx -' 1) = (accum (F (*) h2)) . (nx -' 1) by A91, A112, FINSEQ_4:15;
(accum (F (*) h4)) . (nx + 0) = ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h4) /. ((nx -' 1) + 1)) by A45, A32, A111, A112, A114, Def10
.= ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A111, A110 ;
then A116: ((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1)) = (((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. ((k + 1) + 1))) - ((F (*) h2) /. ((k + 1) + 1)) by A33, A45, A51, A48, A90, FINSEQ_4:15
.= (accum (F (*) h4)) /. (nx -' 1) by RVSUM_1:42 ;
A117: (accum (F (*) h4)) /. (nx -' 1) = (accum (F (*) h4)) . (nx -' 1) by A45, A32, A90, A112, A114, FINSEQ_4:15;
(accum (F (*) h2)) . (nx + 0) = ((accum (F (*) h2)) /. (nx -' 1)) + ((F (*) h2) /. ((nx -' 1) + 1)) by A111, A112, A114, Def10
.= ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. nx) by A64, A111, A112, A113, A115, A117 ;
hence (accum (F (*) h2)) . (nx + 0) = (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A116; :: thesis:

end;

then A118: S₂[ 0 ] ;
A119: for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A118, A92);
A120: i -' nx = i - nx by A88, XREAL_1:233;
then nx <= nx + (i -' nx) by A88;
hence (accum (F (*) h2)) . i = (((accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A89, A119, A120; :: thesis:

end;

A121: (F (*) h2) /. nx = (F (*) h2) . nx by A41, A36, A32, FINSEQ_4:15;
A122: (k + 1) + 1 in dom h4 by A25, A39, FINSEQ_1:def 3;
A123: (F (*) h4) /. ((k + 1) + 1) = (F (*) h4) . ((k + 1) + 1) by A22, A24, A45, FINSEQ_4:15;
A124: for i being Nat st (k + 1) + 1 <= i & i <= len F holds
(accum (F (*) h2)) . i = (accum (F (*) h4)) . i

proof

defpred S₂[ Nat] means ( ((k + 1) + 1) + $1 <= len F implies (accum (F (*) h2)) . (((k + 1) + 1) + $1) = (accum (F (*) h4)) . (((k + 1) + 1) + $1) );
let i be Nat; :: thesis:
assume that
A125: (k + 1) + 1 <= i and
A126: i <= len F ; :: thesis:
A127: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

let k3 be Nat; :: thesis:
assume A128: S₂[k3] ; :: thesis:
( ((k + 1) + 1) + (k3 + 1) <= len F implies (accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = (accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1)) )

proof

A129: (k + 1) + 1 <= ((k + 1) + 1) + k3 by NAT_1:11;
A130: ((k + 1) + 1) + k3 < (((k + 1) + 1) + k3) + 1 by XREAL_1:29;
then A131: (k + 1) + 1 < (((k + 1) + 1) + k3) + 1 by A129, XXREAL_0:2;
assume A132: ((k + 1) + 1) + (k3 + 1) <= len F ; :: thesis:
then A133: (F (*) h4) /. ((((k + 1) + 1) + k3) + 1) = (F (*) h4) . ((((k + 1) + 1) + k3) + 1) by A45, FINSEQ_4:15, NAT_1:11;
1 <= (((k + 1) + 1) + k3) + 1 by NAT_1:11;
then (((k + 1) + 1) + k3) + 1 in Seg (len (F (*) h2)) by A31, A132, FINSEQ_1:1;
then A134: (((k + 1) + 1) + k3) + 1 in dom (F (*) h2) by FINSEQ_1:def 3;
then A135: (F (*) h4) . ((((k + 1) + 1) + k3) + 1) = F . (h4 . ((((k + 1) + 1) + k3) + 1)) by A44, A29, FUNCT_1:12
.= F . (h2b /. ((((k + 1) + 1) + k3) + 1)) by A33, A38, A132, FINSEQ_4:15, NAT_1:11
.= F . (h2r /. ((((k + 1) + 1) + k3) + 1)) by A33, A63, A132, A131, FINSEQ_7:30, NAT_1:11
.= F . (h2r . ((((k + 1) + 1) + k3) + 1)) by A33, A132, FINSEQ_4:15, NAT_1:11
.= (F (*) h2) . ((((k + 1) + 1) + k3) + 1) by A134, FUNCT_1:12 ;
1 <= (k + 1) + 1 by NAT_1:11;
then A136: 1 <= ((k + 1) + 1) + k3 by A129, XXREAL_0:2;
A137: ((k + 1) + 1) + k3 < len F by A132, A130, XXREAL_0:2;
then A138: (accum (F (*) h4)) /. (((k + 1) + 1) + k3) = (accum (F (*) h4)) . (((k + 1) + 1) + k3) by A45, A50, A136, FINSEQ_4:15;
(accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = ((accum (F (*) h2)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1)) by A32, A137, A136, Def10
.= ((accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1)) by A32, A62, A128, A137, A136, A138, FINSEQ_4:15
.= ((accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h4) /. ((((k + 1) + 1) + k3) + 1)) by A32, A132, A135, A133, FINSEQ_4:15, NAT_1:11 ;
hence (accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = (accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1)) by A45, A137, A136, Def10; :: thesis:

end;

hence S₂[k3 + 1] ; :: thesis:

end;

A139: len (accum (F (*) h2)) = len (F (*) h2) by Def10;
A140: (accum (F (*) h2)) . (k + 1) = (((accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A19, A46, A87;
A141: 1 <= k + 1 by NAT_1:11;
k + 1 < len (F (*) h2) by A20, A30, FINSEQ_1:def 3;
then (accum (F (*) h2)) . ((k + 1) + 1) = ((accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A141, Def10
.= ((((accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((k + 1) + 1)) by A20, A32, A139, A140, FINSEQ_4:15, NAT_1:11
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h2) /. nx) by Th4
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1)) by A122, A53, A49, A123, A121, FUNCT_1:13 ;
then A142: S₂[ 0 ] by A20, A18, A45, Def10;
A143: for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A142, A127);
((k + 1) + 1) + (i -' ((k + 1) + 1)) = (i - ((k + 1) + 1)) + ((k + 1) + 1) by A125, XREAL_1:233
.= i ;
hence (accum (F (*) h2)) . i = (accum (F (*) h4)) . i by A126, A143; :: thesis:

end;

A144: (accum F) /. (k + 1) = (accum F) . (k + 1) by A9, A20, FINSEQ_4:15, NAT_1:11;
A145: dom h4 = dom F by A5, FUNCT_2:def 1;
rng h4 c= dom F ;
then A146: dom (F (*) h4) = dom h4 by RELAT_1:27;
then Seg (len (F (*) h4)) = dom h4 by FINSEQ_1:def 3;
then A147: k + 1 < len (F (*) h4) by A20, A145, FINSEQ_1:def 3;
Seg (len (F (*) h4)) = dom F by A145, A146, FINSEQ_1:def 3;
then len (F (*) h4) = len F by FINSEQ_1:def 3;
then A148: (F (*) h4) /. ((k + 1) + 1) = (F (*) h4) . ((k + 1) + 1) by A22, A24, FINSEQ_4:15;
len (accum (F (*) h4)) = len (F (*) h4) by Def10;
then A149: (accum (F (*) h4)) /. (k + 1) = (accum (F (*) h4)) . (k + 1) by A147, FINSEQ_4:15, NAT_1:11;
(accum F) . ((k + 1) + 1) = ((accum F) /. (k + 1)) + (F /. ((k + 1) + 1)) by A10, A20, NAT_1:11
.= ((accum (F (*) h4)) /. (k + 1)) + (F /. ((k + 1) + 1)) by A17, A23, A54, A149, A144
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1)) by A122, A53, A148, A60, FUNCT_1:13
.= (accum (F (*) h4)) . ((k + 1) + 1) by A61, A147, Def10 ;
hence (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) by A22, A124; :: thesis:

end;

suppose nx > k + 1 ; :: thesis:

then A150: (k + 1) + 1 <= nx by NAT_1:13;

per cases ) + 1 = nx or (k + 1) + 1 < nx ) by A150, XXREAL_0:1;

suppose A151: (k + 1) + 1 = nx ; :: thesis:

A152: for i being Nat st k + 1 < i & i <= len F holds
h2 . i = i

proof

let i be Nat; :: thesis:
assume that
A153: k + 1 < i and
A154: i <= len F ; :: thesis:
A155: (k + 1) + 1 <= i by A153, NAT_1:13;

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

suppose (k + 1) + 1 < i ; :: thesis:

hence h2 . i = i by A21, A154; :: thesis:

end;

suppose (k + 1) + 1 = i ; :: thesis:

hence h2 . i = i by A35, A151; :: thesis:

end;

A156: k + 1 < len (F (*) h2) by A20, A30, FINSEQ_1:def 3;
len (accum (F (*) h2)) = len (F (*) h2) by Def10;
then A157: (accum (F (*) h2)) /. (k + 1) = (accum (F (*) h2)) . (k + 1) by A20, A32, FINSEQ_4:15, NAT_1:11;
A158: 1 <= k + 1 by NAT_1:11;
A159: F . ((k + 1) + 1) = (F (*) h2) . nx by A34, A35, FUNCT_1:13;
A160: (accum F) /. (k + 1) = (accum F) . (k + 1) by A9, A20, FINSEQ_4:15, NAT_1:11;
A161: F /. ((k + 1) + 1) = F . ((k + 1) + 1) by A22, A24, FINSEQ_4:15;
(accum F) . ((k + 1) + 1) = ((accum F) /. (k + 1)) + (F /. ((k + 1) + 1)) by A10, A20, NAT_1:11
.= ((accum (F (*) h2)) /. (k + 1)) + (F /. ((k + 1) + 1)) by A17, A23, A152, A157, A160
.= ((accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A22, A24, A32, A151, A161, A159, FINSEQ_4:15
.= (accum (F (*) h2)) . ((k + 1) + 1) by A158, A156, Def10 ;
hence (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) ; :: thesis:

end;

suppose (k + 1) + 1 < nx ; :: thesis:

hence (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) by A21, A35, A36; :: thesis:

end;

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

end;

for h2 being Permutation of (dom F) st ( for i being Nat st 0 + 1 < i & i <= len F holds
h2 . i = i ) holds
(accum F) . (0 + 1) = (accum (F (*) h2)) . (0 + 1)

proof

let h2 be Permutation of (dom F); :: thesis:
A162: rng h2 = dom F by FUNCT_2:def 3;
A163: dom h2 = dom F by A5, FUNCT_2:def 1;
assume A164: for i being Nat st 0 + 1 < i & i <= len F holds
h2 . i = i ; :: thesis:

A165: now :: thesis:

assume A166: h2 . 1 <> 1 ; :: thesis:
consider x being object such that
A167: x in dom h2 and
A168: h2 . x = 1 by A5, A162, FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A163, A167;
1 <= nx by A11, A167, FINSEQ_1:1;
then ( nx = 1 or ( 1 < nx & nx <= len F ) ) by A11, A167, FINSEQ_1:1, XXREAL_0:1;
hence contradiction by A164, A166, A168; :: thesis:

end;

(accum (F (*) h2)) . 1 = (F (*) h2) . 1 by Def10
.= F . 1 by A5, A163, A165, FUNCT_1:13 ;
hence (accum F) . (0 + 1) = (accum (F (*) h2)) . (0 + 1) by Def10; :: thesis:

end;

then A169: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A169, A16);
then (accum F) . (len F) = (accum (F (*) h)) . (len F) by A13, A14, XREAL_1:44
.= (accum F2) . (len F2) by A1, A8, FINSEQ_1:def 3
.= Sum F2 by A12, Def11 ;
hence Sum F2 = Sum F by A2, Def11; :: thesis:

end;

suppose A170: len F <= 0 ; :: thesis:

rng h c= dom F ;
then A171: dom (F (*) h) = dom h by RELAT_1:27;
Seg (len F) = {} by A170;
then dom F = {} by FINSEQ_1:def 3;
then Seg (len F) = dom F2 by A1, A171, FINSEQ_1:def 3;
then A172: len F = len F2 by FINSEQ_1:def 3;
Sum F = 0* n by A170, Def11;
hence Sum F2 = Sum F by A170, A172, Def11; :: thesis:

end;