let n be Nat; :: thesis: for F, F2 being FinSequence of REAL n
for h being Permutation of (dom F) st F2 = F (*) h holds
Sum F2 = Sum F
let F, F2 be FinSequence of REAL n; :: thesis: for h being Permutation of (dom F) st F2 = F (*) h holds
Sum F2 = Sum F
let h be Permutation of (dom F); :: thesis: ( F2 = F (*) h implies Sum F2 = Sum F )
assume A1: F2 = F (*) h ; :: thesis: Sum F2 = Sum F

per cases ( len F > 0 or len F <= 0 ) ;

suppose A2: len F > 0 ; :: thesis: Sum F2 = Sum F

then A3: 0 + 1 <= len F by NAT_1:13;
then A4: 1 in Seg (len F) by FINSEQ_1:3;
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:46;
then A8: Seg (len F2) = dom F by A6, FINSEQ_1:def 3;
set gF = accum F;
A9: len F = len (accum F) by Def11;
A11: for i being Nat st 1 <= i & i < len F holds
(accum F) . (i + 1) = ((accum F) /. i) + (F /. (i + 1)) by Def11;
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);
A13: dom F = Seg (len F) by FINSEQ_1:def 3;
1 in Seg (len F2) by A5, A6, A7, FINSEQ_1:def 3;
then A14: 1 <= len F2 by FINSEQ_1:3;
A15: (len F) -' 1 = (len F) - 1 by A3, XREAL_1:235;
then A16: for i being Nat st ((len F) -' 1) + 1 < i & i <= len F holds
h . i = i ;
A17: dom F <> {} by A4, FINSEQ_1:def 3;
A18: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A19: S₁[k] ; :: thesis: S₁[k + 1]
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

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

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

suppose A48: nx <= k + 1 ; :: thesis: (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1)

A49: (k + 1) + 1 <= len h2r by A22, A35, NAT_1:13;
A50: nx <= len h2r by A13, A36, A35, FINSEQ_1:3;
A51: F . ((k + 1) + 1) = (F (*) h2) . nx by A36, A37, FUNCT_1:23;
A52: len (accum (F (*) h4)) = len (F (*) h4) by Def11;
A53: 1 <= nx by A13, A36, FINSEQ_1:3;
A54: 1 <= (k + 1) + 1 by NAT_1:11;
then A55: h2b . ((k + 1) + 1) = (k + 1) + 1 by A37, A53, A50, A49, Th11;
A56: for i being Nat st k + 1 < i & i <= len F holds
h4 . i = i

proof

let i be Nat; :: thesis: ( k + 1 < i & i <= len F implies h4 . i = i )
assume that
A57: k + 1 < i and
A58: i <= len F ; :: thesis: h4 . i = i
A59: (k + 1) + 1 <= i by A57, NAT_1:13;

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

suppose A60: (k + 1) + 1 < i ; :: thesis: h4 . i = i

1 <= k + 1 by NAT_1:11;
then A61: 1 < i by A57, XXREAL_0:2;
then h4 . i = h2b /. i by A35, A40, A58, FINSEQ_4:24
.= h2r /. i by A35, A48, A57, A58, A60, A61, FINSEQ_7:32
.= h2 . i by A35, A58, A61, FINSEQ_4:24
.= i by A23, A58, A60 ;
hence h4 . i = i ; :: thesis: verum

end;

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

then i = (k + 1) + 1 by A59, XXREAL_0:1;
hence h4 . i = i by A37, A53, A50, A54, A49, Th11; :: thesis: verum

end;

end;

end;

A62: F /. ((k + 1) + 1) = F . ((k + 1) + 1) by A24, A26, FINSEQ_4:24;
A63: 1 <= k + 1 by NAT_1:11;
A64: len (accum (F (*) h2)) = len (F (*) h2) by Def11;
A65: nx < (k + 1) + 1 by A21, A48, XXREAL_0:2;
A66: 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: ( 1 <= i4 & i4 < nx implies (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4 )
assume that
A67: 1 <= i4 and
A68: i4 < nx ; :: thesis: (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4
A69: 1 + (i4 -' 1) = (i4 - 1) + 1 by A67, XREAL_1:235
.= i4 ;
A70: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

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

proof

assume A73: 1 + (k3 + 1) < nx ; :: thesis: (accum (F (*) h2)) . (1 + (k3 + 1)) = (accum (F (*) h4)) . (1 + (k3 + 1))
then A74: 1 + (k3 + 1) < len F by A38, XXREAL_0:2;
then A75: h2r /. ((k3 + 1) + 1) = h2r . ((k3 + 1) + 1) by A35, FINSEQ_4:24, NAT_1:11;
A76: (k3 + 1) + 1 < (k + 1) + 1 by A65, A73, XXREAL_0:2;
A77: h2b /. ((k3 + 1) + 1) = h2b . ((k3 + 1) + 1) by A35, A40, A74, FINSEQ_4:24, NAT_1:11;
1 <= 1 + (k3 + 1) by NAT_1:11;
then (k3 + 1) + 1 in Seg (len F) by A74, FINSEQ_1:3;
then A78: (k3 + 1) + 1 in dom (F (*) h2) by A31, FINSEQ_1:def 3;
then A79: (F (*) h2) . ((k3 + 1) + 1) = F . (h2 . ((k3 + 1) + 1)) by FUNCT_1:22
.= F . (h4 . ((k3 + 1) + 1)) by A35, A73, A74, A76, A75, A77, FINSEQ_7:32, NAT_1:11
.= (F (*) h4) . ((k3 + 1) + 1) by A46, A31, A78, FUNCT_1:22 ;
A80: (F (*) h4) /. ((k3 + 1) + 1) = (F (*) h4) . ((k3 + 1) + 1) by A47, A74, FINSEQ_4:24, NAT_1:11;
A81: k3 + 1 < 1 + (k3 + 1) by XREAL_1:31;
then A82: k3 + 1 < nx by A73, XXREAL_0:2;
then A83: k3 + 1 < len F by A38, XXREAL_0:2;
k3 + 1 < len (F (*) h2) by A38, A34, A82, XXREAL_0:2;
then A84: (accum (F (*) h4)) /. (1 + k3) = (accum (F (*) h4)) . (1 + k3) by A47, A34, A52, FINSEQ_4:24, NAT_1:11;
(accum (F (*) h2)) /. (1 + k3) = (accum (F (*) h2)) . (1 + k3) by A34, A64, A83, FINSEQ_4:24, NAT_1:11;
then (accum (F (*) h2)) . (1 + (k3 + 1)) = ((accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h2) /. ((k3 + 1) + 1)) by A34, A72, A71, A73, A81, A83, A84, Def11, XXREAL_0:2
.= ((accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h4) /. ((k3 + 1) + 1)) by A34, A74, A79, A80, FINSEQ_4:24, NAT_1:11 ;
hence (accum (F (*) h2)) . (1 + (k3 + 1)) = (accum (F (*) h4)) . (1 + (k3 + 1)) by A47, A71, A83, Def11; :: thesis: verum

end;

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

end;

0 < k + 1 ;
then A85: 1 <> (k + 1) + 1 ;
A86: h2b /. 1 = h2b . 1 by A3, A35, A40, FINSEQ_4:24;
A87: h2r /. 1 = h2r . 1 by A3, A35, FINSEQ_4:24;
(F (*) h2) . 1 = F . (h2 . 1) by A5, A31, FUNCT_1:22
.= F . (h4 . 1) by A3, A35, A67, A68, A85, A87, A86, FINSEQ_7:32
.= (F (*) h4) . 1 by A5, A46, FUNCT_1:22 ;
then (accum (F (*) h2)) . (1 + 0) = (F (*) h4) . 1 by Def11
.= (accum (F (*) h4)) . (1 + 0) by Def11 ;
then A88: S₂[ 0 ] ;
for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A88, A70);
hence (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4 by A68, A69; :: thesis: verum

end;

A89: 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: ( nx <= i & i < (k + 1) + 1 implies (accum (F (*) h2)) . i = (((accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) )
assume that
A90: nx <= i and
A91: i < (k + 1) + 1 ; :: thesis: (accum (F (*) h2)) . i = (((accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)
A92: len (accum (F (*) h4)) = len (F (*) h4) by Def11;
A93: len (accum (F (*) h2)) = len (F (*) h2) by Def11;
A94: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

let k3 be Nat; :: thesis: ( S₂[k3] implies S₂[k3 + 1] )
assume A95: S₂[k3] ; :: thesis: S₂[k3 + 1]
( 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 ;
A96: nx <= nx + k3 by NAT_1:11;
reconsider f2 = (F (*) h2) /. ((k + 1) + 1) as Element of REAL n ;
A97: nx + k3 < (nx + k3) + 1 by XREAL_1:31;
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
A98: nx + (k3 + 1) < (k + 1) + 1 ; :: thesis: (accum (F (*) h2)) . (nx + (k3 + 1)) = (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)
A99: nx + (k3 + 1) < len (accum (F (*) h4)) by A24, A47, A92, A98, XXREAL_0:2;
A100: nx + k3 < (nx + k3) + 1 by XREAL_1:31;
then nx + k3 < (k + 1) + 1 by A98, XXREAL_0:2;
then A101: nx + k3 < len (F (*) h2) by A35, A34, A49, XXREAL_0:2;
then A102: (nx + k3) + 1 <= len (F (*) h2) by NAT_1:13;
nx + k3 >= 0 + 1 by A43, NAT_1:13;
then A103: 1 < nx + (k3 + 1) by A100, XXREAL_0:2;
then A104: (F (*) h4) /. ((nx + k3) + 1) = (F (*) h4) . ((nx + k3) + 1) by A47, A34, A102, FINSEQ_4:24;
(nx + k3) + 1 in Seg (len (F (*) h2)) by A103, A102, FINSEQ_1:3;
then A105: (nx + k3) + 1 in dom (F (*) h2) by FINSEQ_1:def 3;
then A106: (F (*) h4) . ((nx + k3) + 1) = F . (h4 . ((nx + k3) + 1)) by A46, A31, FUNCT_1:22
.= F . (h2b /. ((nx + k3) + 1)) by A35, A40, A34, A103, A102, FINSEQ_4:24
.= F . (h2r /. ((nx + k3) + 1)) by A35, A34, A98, A103, A102, A97, A96, FINSEQ_7:32
.= F . (h2r . ((nx + k3) + 1)) by A35, A34, A103, A102, FINSEQ_4:24
.= (F (*) h2) . ((nx + k3) + 1) by A105, FUNCT_1:22 ;
nx <= nx + k3 by NAT_1:11;
then A107: 1 <= nx + k3 by A53, XXREAL_0:2;
then (accum (F (*) h4)) . (nx + (k3 + 1)) = ((accum (F (*) h4)) /. (nx + k3)) + ((F (*) h4) /. ((nx + k3) + 1)) by A47, A34, A101, Def11
.= ((accum (F (*) h4)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1)) by A103, A102, A106, A104, FINSEQ_4:24 ;
then A108: (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) = ((f1 + f3) - f2) + f4 by A103, A99, FINSEQ_4:24
.= ((f1 - f2) + f3) + f4 by RFUNCT_1:19
.= ((f1 - f2) + f4) + f3 by RFUNCT_1:19 ;
(accum (F (*) h2)) . (nx + (k3 + 1)) = ((accum (F (*) h2)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1)) by A107, A101, Def11
.= ((((accum (F (*) h4)) /. (nx + k3)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((nx + k3) + 1)) by A93, A95, A98, A100, A107, A101, FINSEQ_4:24, 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 A108; :: thesis: verum

end;

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

end;

now

per cases ( 1 = nx or 1 < nx ) by A43, XXREAL_0:1;

case A109: 1 = nx ; :: thesis: (accum (F (*) h2)) . (nx + 0) = (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)

A110: n in NAT by ORDINAL1:def 13;
(accum (F (*) h4)) /. (nx + 0) = (accum (F (*) h4)) . 1 by A3, A47, A92, A109, FINSEQ_4:24
.= (F (*) h4) . 1 by Def11
.= F . (h2 . ((k + 1) + 1)) by A5, A45, A44, A109, FUNCT_1:23
.= (F (*) h2) . ((k + 1) + 1) by A29, A28, FUNCT_1:23
.= (F (*) h2) /. ((k + 1) + 1) by A24, A26, A34, FINSEQ_4:24 ;
then A111: (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) = (0* n) + ((F (*) h2) /. nx) by A110, EUCLIDLP:7
.= (F (*) h2) /. nx by EUCLID_4:1 ;
(accum (F (*) h2)) . (nx + 0) = (F (*) h2) . 1 by A109, Def11
.= (F (*) h2) /. nx by A38, A34, A109, FINSEQ_4:24 ;
hence (accum (F (*) h2)) . (nx + 0) = (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A111; :: thesis: verum

end;

case A112: 1 < nx ; :: thesis: (accum (F (*) h2)) . (nx + 0) = (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)

A113: (F (*) h4) /. nx = (F (*) h4) . nx by A43, A38, A47, FINSEQ_4:24
.= F . (h2 . ((k + 1) + 1)) by A36, A45, A44, FUNCT_1:23
.= (F (*) h2) . ((k + 1) + 1) by A29, A28, FUNCT_1:23
.= (F (*) h2) /. ((k + 1) + 1) by A24, A26, A34, FINSEQ_4:24 ;
A114: nx -' 1 = nx - 1 by A112, XREAL_1:235;
then nx -' 1 > 0 by A112, XREAL_1:52;
then A115: nx -' 1 >= 0 + 1 by NAT_1:13;
nx < nx + 1 by XREAL_1:31;
then A116: nx - 1 < (nx + 1) - 1 by XREAL_1:11;
then A117: nx -' 1 < len (F (*) h2) by A35, A34, A50, A114, XXREAL_0:2;
then A118: (accum (F (*) h2)) /. (nx -' 1) = (accum (F (*) h2)) . (nx -' 1) by A93, A115, FINSEQ_4:24;
(accum (F (*) h4)) . (nx + 0) = ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h4) /. ((nx -' 1) + 1)) by A47, A34, A114, A115, A117, Def11
.= ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A114, A113 ;
then A119: ((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 A35, A47, A53, A50, A92, FINSEQ_4:24
.= (accum (F (*) h4)) /. (nx -' 1) by RVSUM_1:63 ;
A120: (accum (F (*) h4)) /. (nx -' 1) = (accum (F (*) h4)) . (nx -' 1) by A47, A34, A92, A115, A117, FINSEQ_4:24;
(accum (F (*) h2)) . (nx + 0) = ((accum (F (*) h2)) /. (nx -' 1)) + ((F (*) h2) /. ((nx -' 1) + 1)) by A114, A115, A117, Def11
.= ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. nx) by A66, A114, A115, A116, A118, A120 ;
hence (accum (F (*) h2)) . (nx + 0) = (((accum (F (*) h4)) /. (nx + 0)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A119; :: thesis: verum

end;

end;

end;

then A121: S₂[ 0 ] ;
A122: for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A121, A94);
A123: i -' nx = i - nx by A90, XREAL_1:235;
then nx <= nx + (i -' nx) by A90;
hence (accum (F (*) h2)) . i = (((accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A91, A122, A123; :: thesis: verum

end;

A124: (F (*) h2) /. nx = (F (*) h2) . nx by A43, A38, A34, FINSEQ_4:24;
A125: (k + 1) + 1 in dom h4 by A27, A41, FINSEQ_1:def 3;
A126: (F (*) h4) /. ((k + 1) + 1) = (F (*) h4) . ((k + 1) + 1) by A24, A26, A47, FINSEQ_4:24;
A127: 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: ( (k + 1) + 1 <= i & i <= len F implies (accum (F (*) h2)) . i = (accum (F (*) h4)) . i )
assume that
A128: (k + 1) + 1 <= i and
A129: i <= len F ; :: thesis: (accum (F (*) h2)) . i = (accum (F (*) h4)) . i
A130: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

let k3 be Nat; :: thesis: ( S₂[k3] implies S₂[k3 + 1] )
assume A131: S₂[k3] ; :: thesis: S₂[k3 + 1]
( ((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

A132: (k + 1) + 1 <= ((k + 1) + 1) + k3 by NAT_1:11;
A133: ((k + 1) + 1) + k3 < (((k + 1) + 1) + k3) + 1 by XREAL_1:31;
then A134: (k + 1) + 1 < (((k + 1) + 1) + k3) + 1 by A132, XXREAL_0:2;
assume A135: ((k + 1) + 1) + (k3 + 1) <= len F ; :: thesis: (accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = (accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1))
then A136: (F (*) h4) /. ((((k + 1) + 1) + k3) + 1) = (F (*) h4) . ((((k + 1) + 1) + k3) + 1) by A47, FINSEQ_4:24, 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 A33, A135, FINSEQ_1:3;
then A137: (((k + 1) + 1) + k3) + 1 in dom (F (*) h2) by FINSEQ_1:def 3;
then A138: (F (*) h4) . ((((k + 1) + 1) + k3) + 1) = F . (h4 . ((((k + 1) + 1) + k3) + 1)) by A46, A31, FUNCT_1:22
.= F . (h2b /. ((((k + 1) + 1) + k3) + 1)) by A35, A40, A135, FINSEQ_4:24, NAT_1:11
.= F . (h2r /. ((((k + 1) + 1) + k3) + 1)) by A35, A65, A135, A134, FINSEQ_7:32, NAT_1:11
.= F . (h2r . ((((k + 1) + 1) + k3) + 1)) by A35, A135, FINSEQ_4:24, NAT_1:11
.= (F (*) h2) . ((((k + 1) + 1) + k3) + 1) by A137, FUNCT_1:22 ;
1 <= (k + 1) + 1 by NAT_1:11;
then A139: 1 <= ((k + 1) + 1) + k3 by A132, XXREAL_0:2;
A140: ((k + 1) + 1) + k3 < len F by A135, A133, XXREAL_0:2;
then A141: (accum (F (*) h4)) /. (((k + 1) + 1) + k3) = (accum (F (*) h4)) . (((k + 1) + 1) + k3) by A47, A52, A139, FINSEQ_4:24;
(accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = ((accum (F (*) h2)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1)) by A34, A140, A139, Def11
.= ((accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1)) by A34, A64, A131, A140, A139, A141, FINSEQ_4:24
.= ((accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h4) /. ((((k + 1) + 1) + k3) + 1)) by A34, A135, A138, A136, FINSEQ_4:24, NAT_1:11 ;
hence (accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = (accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1)) by A47, A140, A139, Def11; :: thesis: verum

end;

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

end;

A142: len (accum (F (*) h2)) = len (F (*) h2) by Def11;
A143: (accum (F (*) h2)) . (k + 1) = (((accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A21, A48, A89;
A144: 1 <= k + 1 by NAT_1:11;
k + 1 < len (F (*) h2) by A22, A32, FINSEQ_1:def 3;
then (accum (F (*) h2)) . ((k + 1) + 1) = ((accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A144, Def11
.= ((((accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((k + 1) + 1)) by A22, A34, A142, A143, FINSEQ_4:24, NAT_1:11
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h2) /. nx) by Th6
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1)) by A125, A55, A51, A126, A124, FUNCT_1:23 ;
then A145: S₂[ 0 ] by A22, A20, A47, Def11;
A146: for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A145, A130);
((k + 1) + 1) + (i -' ((k + 1) + 1)) = (i - ((k + 1) + 1)) + ((k + 1) + 1) by A128, XREAL_1:235
.= i ;
hence (accum (F (*) h2)) . i = (accum (F (*) h4)) . i by A129, A146; :: thesis: verum

end;

A147: (accum F) /. (k + 1) = (accum F) . (k + 1) by A9, A22, FINSEQ_4:24, NAT_1:11;
A148: dom h4 = dom F by A5, FUNCT_2:def 1;
rng h4 c= dom F ;
then A149: dom (F (*) h4) = dom h4 by RELAT_1:46;
then Seg (len (F (*) h4)) = dom h4 by FINSEQ_1:def 3;
then A150: k + 1 < len (F (*) h4) by A22, A148, FINSEQ_1:def 3;
Seg (len (F (*) h4)) = dom F by A148, A149, FINSEQ_1:def 3;
then len (F (*) h4) = len F by FINSEQ_1:def 3;
then A151: (F (*) h4) /. ((k + 1) + 1) = (F (*) h4) . ((k + 1) + 1) by A24, A26, FINSEQ_4:24;
len (accum (F (*) h4)) = len (F (*) h4) by Def11;
then A152: (accum (F (*) h4)) /. (k + 1) = (accum (F (*) h4)) . (k + 1) by A150, FINSEQ_4:24, NAT_1:11;
(accum F) . ((k + 1) + 1) = ((accum F) /. (k + 1)) + (F /. ((k + 1) + 1)) by A11, A22, NAT_1:11
.= ((accum (F (*) h4)) /. (k + 1)) + (F /. ((k + 1) + 1)) by A19, A25, A56, A152, A147
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1)) by A125, A55, A151, A62, FUNCT_1:23
.= (accum (F (*) h4)) . ((k + 1) + 1) by A63, A150, Def11 ;
hence (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) by A24, A127; :: thesis: verum

end;

suppose nx > k + 1 ; :: thesis: (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1)

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

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

suppose A154: (k + 1) + 1 = nx ; :: thesis: (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1)

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

proof

let i be Nat; :: thesis: ( k + 1 < i & i <= len F implies h2 . i = i )
assume that
A156: k + 1 < i and
A157: i <= len F ; :: thesis: h2 . i = i
A158: (k + 1) + 1 <= i by A156, NAT_1:13;

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

suppose (k + 1) + 1 < i ; :: thesis: h2 . i = i

hence h2 . i = i by A23, A157; :: thesis: verum

end;

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

hence h2 . i = i by A37, A154; :: thesis: verum

end;

end;

end;

A159: k + 1 < len (F (*) h2) by A22, A32, FINSEQ_1:def 3;
len (accum (F (*) h2)) = len (F (*) h2) by Def11;
then A160: (accum (F (*) h2)) /. (k + 1) = (accum (F (*) h2)) . (k + 1) by A22, A34, FINSEQ_4:24, NAT_1:11;
A161: 1 <= k + 1 by NAT_1:11;
A162: F . ((k + 1) + 1) = (F (*) h2) . nx by A36, A37, FUNCT_1:23;
A163: (accum F) /. (k + 1) = (accum F) . (k + 1) by A9, A22, FINSEQ_4:24, NAT_1:11;
A164: F /. ((k + 1) + 1) = F . ((k + 1) + 1) by A24, A26, FINSEQ_4:24;
(accum F) . ((k + 1) + 1) = ((accum F) /. (k + 1)) + (F /. ((k + 1) + 1)) by A11, A22, NAT_1:11
.= ((accum (F (*) h2)) /. (k + 1)) + (F /. ((k + 1) + 1)) by A19, A25, A155, A160, A163
.= ((accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A24, A26, A34, A154, A164, A162, FINSEQ_4:24
.= (accum (F (*) h2)) . ((k + 1) + 1) by A161, A159, Def11 ;
hence (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) ; :: thesis: verum

end;

suppose (k + 1) + 1 < nx ; :: thesis: (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1)

hence (accum F) . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) by A23, A37, A38; :: thesis: verum

end;

end;

end;

end;

end;

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

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: ( ( for i being Nat st 0 + 1 < i & i <= len F holds
h2 . i = i ) implies (accum F) . (0 + 1) = (accum (F (*) h2)) . (0 + 1) )
A165: rng h2 = dom F by FUNCT_2:def 3;
A166: dom h2 = dom F by A5, FUNCT_2:def 1;
assume A167: for i being Nat st 0 + 1 < i & i <= len F holds
h2 . i = i ; :: thesis: (accum F) . (0 + 1) = (accum (F (*) h2)) . (0 + 1)

A168: now

assume A169: h2 . 1 <> 1 ; :: thesis: contradiction
consider x being set such that
A170: x in dom h2 and
A171: h2 . x = 1 by A5, A165, FUNCT_1:def 5;
reconsider nx = x as Element of NAT by A166, A170;
1 <= nx by A13, A170, FINSEQ_1:3;
then ( nx = 1 or ( 1 < nx & nx <= len F ) ) by A13, A170, FINSEQ_1:3, XXREAL_0:1;
hence contradiction by A167, A169, A171; :: thesis: verum

end;

(accum (F (*) h2)) . 1 = (F (*) h2) . 1 by Def11
.= F . 1 by A5, A166, A168, FUNCT_1:23 ;
hence (accum F) . (0 + 1) = (accum (F (*) h2)) . (0 + 1) by Def11; :: thesis: verum

end;

then A172: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A172, A18);
then (accum F) . (len F) = (accum (F (*) h)) . (len F) by A15, A16, XREAL_1:46
.= (accum F2) . (len F2) by A1, A8, FINSEQ_1:def 3
.= Sum F2 by A14, Def10 ;
hence Sum F2 = Sum F by A2, Def10; :: thesis: verum

end;

suppose A173: len F <= 0 ; :: thesis: Sum F2 = Sum F

rng h c= dom F ;
then A174: dom (F (*) h) = dom h by RELAT_1:46;
Seg (len F) = {} by A173;
then dom F = {} by FINSEQ_1:def 3;
then Seg (len F) = dom F2 by A1, A174, FINSEQ_1:def 3;
then A175: len F = len F2 by FINSEQ_1:def 3;
Sum F = 0* n by A173, Def10;
hence Sum F2 = Sum F by A173, A175, Def10; :: thesis: verum

end;

end;