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 consider gF being FinSequence of REAL n such that
A3: ( len F = len gF & F . 1 = gF . 1 & ( for i being Nat st 1 <= i & i < len F holds
gF . (i + 1) = (gF /. i) + (F /. (i + 1)) ) & Sum F = gF . (len F) ) by Def11;
A4: 0 + 1 <= len F by A2, NAT_1:13;
then A5: 1 in Seg (len F) by FINSEQ_1:3;
then A6: 1 in dom F by FINSEQ_1:def 3;
A7: dom F <> {} by A5, FINSEQ_1:def 3;
A8: dom h = dom F by A6, FUNCT_2:def 1;
A9: dom F = Seg (len F) by FINSEQ_1:def 3;
rng h = dom h by A8, FUNCT_2:def 3;
then A10: ( dom F2 = dom h & rng F2 = rng F ) by A8, A1, RELAT_1:46, RELAT_1:47;
then A11: Seg (len F2) = dom F by A8, FINSEQ_1:def 3;
1 in Seg (len F2) by A6, A8, A10, FINSEQ_1:def 3;
then A12: 1 <= len F2 by FINSEQ_1:3;
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
gF . ($1 + 1) = (accum (F (*) h2)) . ($1 + 1);
for h2 being Permutation of (dom F) st ( for i being Nat st 0 + 1 < i & i <= len F holds
h2 . i = i ) holds
gF . (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 gF . (0 + 1) = (accum (F (*) h2)) . (0 + 1) )
assume A13: for i being Nat st 0 + 1 < i & i <= len F holds
h2 . i = i ; :: thesis: gF . (0 + 1) = (accum (F (*) h2)) . (0 + 1)
A14: dom h2 = dom F by A6, FUNCT_2:def 1;
A15: rng h2 = dom F by FUNCT_2:def 3;

A16: now

assume A17: h2 . 1 <> 1 ; :: thesis: contradiction
consider x being set such that
A18: ( x in dom h2 & h2 . x = 1 ) by A6, A15, FUNCT_1:def 5;
reconsider nx = x as Element of NAT by A18, A14;
( 1 <= nx & nx <= len F ) by A18, A9, FINSEQ_1:3;
then ( nx = 1 or ( 1 < nx & nx <= len F ) ) by XXREAL_0:1;
hence contradiction by A13, A17, A18; :: thesis: verum

end;

(accum (F (*) h2)) . 1 = (F (*) h2) . 1 by Def12
.= F . 1 by A6, A14, A16, FUNCT_1:23 ;
hence gF . (0 + 1) = (accum (F (*) h2)) . (0 + 1) by A3; :: thesis: verum

end;

then A19: S₁[ 0 ] ;
A20: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A21: 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
gF . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1)

proof

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

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

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

then A50: nx < (k + 1) + 1 by A26, XXREAL_0:2;
A51: (k + 1) + 1 in dom h4 by A31, A38, FINSEQ_1:def 3;
A52: ( 1 <= nx & nx <= len h2r & 1 <= (k + 1) + 1 & (k + 1) + 1 <= len h2r ) by A9, A22, A32, A36, FINSEQ_1:3, NAT_1:11, NAT_1:13;
then A53: h2b . ((k + 1) + 1) = (k + 1) + 1 by Th13, A32;
A54: F . ((k + 1) + 1) = (F (*) h2) . nx by A32, FUNCT_1:23;
A55: (F (*) h4) /. ((k + 1) + 1) = (F (*) h4) . ((k + 1) + 1) by A25, A30, A43, FINSEQ_4:24;
A56: (F (*) h2) /. nx = (F (*) h2) . nx by A34, A48, FINSEQ_4:24;
A57: dom h4 = dom F by A6, FUNCT_2:def 1;
A58: 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 A59: ( k + 1 < i & i <= len F ) ; :: thesis: h4 . i = i
then A60: (k + 1) + 1 <= i by NAT_1:13;

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

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

1 <= k + 1 by NAT_1:11;
then A62: 1 < i by A59, XXREAL_0:2;
then h4 . i = h2b /. i by A37, A36, A59, FINSEQ_4:24
.= h2r /. i by A36, A49, A59, A61, A62, FINSEQ_7:32
.= h2 . i by A62, A59, A36, FINSEQ_4:24
.= i by A22, A61, A59 ;
hence h4 . i = i ; :: thesis: verum

end;

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

then i = (k + 1) + 1 by A60, XXREAL_0:1;
hence h4 . i = i by A32, A52, Th13; :: thesis: verum

end;

end;

end;

A63: len (accum (F (*) h4)) = len (F (*) h4) by Def12;
A64: len (accum (F (*) h2)) = len (F (*) h2) by Def12;
A65: for i4 being Nat st 1 <= i4 & i4 < nx holds
(accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4

proof

let i4 be Nat; :: thesis: ( 1 <= i4 & i4 < nx implies (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4 )
assume A66: ( 1 <= i4 & i4 < nx ) ; :: thesis: (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4
defpred S₂[ Nat] means ( 1 + $1 < nx implies (accum (F (*) h2)) . (1 + $1) = (accum (F (*) h4)) . (1 + $1) );
0 < k + 1 ;
then A67: 1 <> (k + 1) + 1 ;
A68: h2r /. 1 = h2r . 1 by A4, A36, FINSEQ_4:24;
A69: h2b /. 1 = h2b . 1 by A4, A36, A37, FINSEQ_4:24;
(F (*) h2) . 1 = F . (h2 . 1) by A6, A45, FUNCT_1:22
.= F . (h4 . 1) by A4, A36, A66, A67, A68, A69, FINSEQ_7:32
.= (F (*) h4) . 1 by A6, A42, FUNCT_1:22 ;
then (accum (F (*) h2)) . (1 + 0 ) = (F (*) h4) . 1 by Def12
.= (accum (F (*) h4)) . (1 + 0 ) by Def12 ;
then A70: S₂[ 0 ] ;
A71: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

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

proof

assume A74: 1 + (k3 + 1) < nx ; :: thesis: (accum (F (*) h2)) . (1 + (k3 + 1)) = (accum (F (*) h4)) . (1 + (k3 + 1))
then A75: 1 + (k3 + 1) < len F by A34, XXREAL_0:2;
1 <= 1 + (k3 + 1) by NAT_1:11;
then A76: (k3 + 1) + 1 in Seg (len F) by A75, FINSEQ_1:3;
A77: k3 + 1 < 1 + (k3 + 1) by XREAL_1:31;
then A78: k3 + 1 < nx by A74, XXREAL_0:2;
then A79: k3 + 1 < len F by A34, XXREAL_0:2;
A80: k3 + 1 < len (F (*) h2) by A34, A48, A78, XXREAL_0:2;
A81: (accum (F (*) h2)) /. (1 + k3) = (accum (F (*) h2)) . (1 + k3) by A48, A64, A79, FINSEQ_4:24, NAT_1:11;
A82: (accum (F (*) h4)) /. (1 + k3) = (accum (F (*) h4)) . (1 + k3) by A43, A48, A63, A80, FINSEQ_4:24, NAT_1:11;
A83: (k3 + 1) + 1 < (k + 1) + 1 by A50, A74, XXREAL_0:2;
A84: h2r /. ((k3 + 1) + 1) = h2r . ((k3 + 1) + 1) by A36, A75, FINSEQ_4:24, NAT_1:11;
A85: h2b /. ((k3 + 1) + 1) = h2b . ((k3 + 1) + 1) by A36, A37, A75, FINSEQ_4:24, NAT_1:11;
A86: (k3 + 1) + 1 in dom (F (*) h2) by A76, A45, FINSEQ_1:def 3;
then A87: (F (*) h2) . ((k3 + 1) + 1) = F . (h2 . ((k3 + 1) + 1)) by FUNCT_1:22
.= F . (h4 . ((k3 + 1) + 1)) by A36, A74, A75, A83, A84, A85, FINSEQ_7:32, NAT_1:11
.= (F (*) h4) . ((k3 + 1) + 1) by A86, A42, A45, FUNCT_1:22 ;
A88: (F (*) h4) /. ((k3 + 1) + 1) = (F (*) h4) . ((k3 + 1) + 1) by A43, A75, FINSEQ_4:24, NAT_1:11;
(accum (F (*) h2)) . (1 + (k3 + 1)) = ((accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h2) /. ((k3 + 1) + 1)) by A48, A73, A79, Def12, A72, A74, A77, A81, A82, XXREAL_0:2
.= ((accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h4) /. ((k3 + 1) + 1)) by A48, A75, A87, A88, FINSEQ_4:24, NAT_1:11 ;
hence (accum (F (*) h2)) . (1 + (k3 + 1)) = (accum (F (*) h4)) . (1 + (k3 + 1)) by A43, A73, A79, Def12; :: thesis: verum

end;

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

end;

A89: for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A70, A71);
1 + (i4 -' 1) = (i4 - 1) + 1 by A66, XREAL_1:235
.= i4 ;
hence (accum (F (*) h2)) . i4 = (accum (F (*) h4)) . i4 by A66, A89; :: thesis: verum

end;

A90: 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

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 A91: ( nx <= i & i < (k + 1) + 1 ) ; :: thesis: (accum (F (*) h2)) . i = (((accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)
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) );
A92: len (accum (F (*) h4)) = len (F (*) h4) by Def12;
A93: len (accum (F (*) h2)) = len (F (*) h2) by Def12;

now

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

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

then A95: (accum (F (*) h2)) . (nx + 0 ) = (F (*) h2) . 1 by Def12
.= (F (*) h2) /. nx by A34, A48, A94, FINSEQ_4:24 ;
A96: n in NAT by ORDINAL1:def 13;
(accum (F (*) h4)) /. (nx + 0 ) = (accum (F (*) h4)) . 1 by A94, A92, A43, A4, FINSEQ_4:24
.= (F (*) h4) . 1 by Def12
.= F . (h2 . ((k + 1) + 1)) by A6, A41, A44, A94, FUNCT_1:23
.= (F (*) h2) . ((k + 1) + 1) by A33, A23, FUNCT_1:23
.= (F (*) h2) /. ((k + 1) + 1) by A25, A30, A48, FINSEQ_4:24 ;
then (((accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) = (0* n) + ((F (*) h2) /. nx) by A96, EUCLIDLP:7
.= (F (*) h2) /. nx by EUCLID_4:1 ;
hence (accum (F (*) h2)) . (nx + 0 ) = (((accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A95; :: thesis: verum

end;

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

then A98: nx -' 1 = nx - 1 by XREAL_1:235;
then nx -' 1 > 0 by A97, XREAL_1:52;
then A99: nx -' 1 >= 0 + 1 by NAT_1:13;
nx < nx + 1 by XREAL_1:31;
then A100: nx - 1 < (nx + 1) - 1 by XREAL_1:11;
then A101: nx -' 1 < len (F (*) h2) by A36, A48, A52, A98, XXREAL_0:2;
then A102: (accum (F (*) h2)) /. (nx -' 1) = (accum (F (*) h2)) . (nx -' 1) by A93, A99, FINSEQ_4:24;
A103: (accum (F (*) h4)) /. (nx -' 1) = (accum (F (*) h4)) . (nx -' 1) by A43, A48, A92, A99, A101, FINSEQ_4:24;
A104: (F (*) h4) /. nx = (F (*) h4) . nx by A34, A43, FINSEQ_4:24
.= F . (h2 . ((k + 1) + 1)) by A32, A41, A44, FUNCT_1:23
.= (F (*) h2) . ((k + 1) + 1) by A23, A33, FUNCT_1:23
.= (F (*) h2) /. ((k + 1) + 1) by A25, A30, A48, FINSEQ_4:24 ;
A105: (accum (F (*) h2)) . (nx + 0 ) = ((accum (F (*) h2)) /. (nx -' 1)) + ((F (*) h2) /. ((nx -' 1) + 1)) by A98, A99, A101, Def12
.= ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. nx) by A65, A98, A99, A100, A102, A103 ;
(accum (F (*) h4)) . (nx + 0 ) = ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h4) /. ((nx -' 1) + 1)) by A98, A43, A48, A99, A101, Def12
.= ((accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A98, A104 ;
then ((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 A36, A43, A52, A92, FINSEQ_4:24
.= (accum (F (*) h4)) /. (nx -' 1) by RVSUM_1:63 ;
hence (accum (F (*) h2)) . (nx + 0 ) = (((accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A105; :: thesis: verum

end;

end;

end;

then A106: S₂[ 0 ] ;
A107: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

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

assume A109: ( nx <= nx + (k3 + 1) & 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)
A110: nx <= nx + k3 by NAT_1:11;
A111: nx + k3 >= 0 + 1 by A34, NAT_1:13;
A112: nx + k3 < (nx + k3) + 1 by XREAL_1:31;
then A113: 1 < nx + (k3 + 1) by A111, XXREAL_0:2;
A114: nx + (k3 + 1) < len (accum (F (*) h4)) by A25, A43, A92, A109, XXREAL_0:2;
nx + k3 < (k + 1) + 1 by A109, A112, XXREAL_0:2;
then A115: ( 1 <= nx + k3 & nx + k3 < len (F (*) h2) ) by A36, A48, A52, A110, XXREAL_0:2;
then A116: (nx + k3) + 1 <= len (F (*) h2) by NAT_1:13;
A117: nx + k3 < (nx + k3) + 1 by XREAL_1:31;
A118: nx <= nx + k3 by NAT_1:11;
(nx + k3) + 1 in Seg (len (F (*) h2)) by A116, A113, FINSEQ_1:3;
then A119: (nx + k3) + 1 in dom (F (*) h2) by FINSEQ_1:def 3;
then A120: (F (*) h4) . ((nx + k3) + 1) = F . (h4 . ((nx + k3) + 1)) by A42, A45, FUNCT_1:22
.= F . (h2b /. ((nx + k3) + 1)) by A37, A36, A116, A113, A48, FINSEQ_4:24
.= F . (h2r /. ((nx + k3) + 1)) by A36, A48, A109, A113, A116, A117, A118, FINSEQ_7:32
.= F . (h2r . ((nx + k3) + 1)) by A36, A116, A113, A48, FINSEQ_4:24
.= (F (*) h2) . ((nx + k3) + 1) by A119, FUNCT_1:22 ;
A121: (F (*) h4) /. ((nx + k3) + 1) = (F (*) h4) . ((nx + k3) + 1) by A116, A113, A43, A48, FINSEQ_4:24;
A122: (accum (F (*) h2)) . (nx + (k3 + 1)) = ((accum (F (*) h2)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1)) by Def12, A115
.= ((((accum (F (*) h4)) /. (nx + k3)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((nx + k3) + 1)) by A93, A108, A109, A112, A115, FINSEQ_4:24, NAT_1:11, XXREAL_0:2 ;
reconsider f1 = (accum (F (*) h4)) /. (nx + k3) as Element of REAL n ;
reconsider f2 = (F (*) h2) /. ((k + 1) + 1) as Element of REAL n ;
reconsider f3 = (F (*) h2) /. ((nx + k3) + 1) as Element of REAL n ;
reconsider f4 = (F (*) h2) /. nx as Element of REAL n ;
(accum (F (*) h4)) . (nx + (k3 + 1)) = ((accum (F (*) h4)) /. (nx + k3)) + ((F (*) h4) /. ((nx + k3) + 1)) by Def12, A115, A43, A48
.= ((accum (F (*) h4)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1)) by A113, A116, A120, A121, FINSEQ_4:24 ;
then (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) = ((f1 + f3) - f2) + f4 by A113, A114, FINSEQ_4:24
.= ((f1 - f2) + f3) + f4 by RFUNCT_1:19
.= ((f1 - f2) + f4) + f3 by RFUNCT_1:19 ;
hence (accum (F (*) h2)) . (nx + (k3 + 1)) = (((accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A122; :: thesis: verum

end;

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

end;

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

end;

A125: for i being Nat st (k + 1) + 1 <= i & i <= len F holds
(accum (F (*) h2)) . i = (accum (F (*) h4)) . i

proof

let i be Nat; :: thesis: ( (k + 1) + 1 <= i & i <= len F implies (accum (F (*) h2)) . i = (accum (F (*) h4)) . i )
assume A126: ( (k + 1) + 1 <= i & i <= len F ) ; :: thesis: (accum (F (*) h2)) . i = (accum (F (*) h4)) . i
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) );
A127: len (accum (F (*) h2)) = len (F (*) h2) by Def12;
A128: ( 1 <= k + 1 & k + 1 < len (F (*) h2) ) by A22, A46, FINSEQ_1:def 3, NAT_1:11;
A129: (accum (F (*) h2)) . (k + 1) = (((accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx) by A26, A49, A90;
(accum (F (*) h2)) . ((k + 1) + 1) = ((accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A128, Def12
.= ((((accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((k + 1) + 1)) by A27, A48, A127, A129, FINSEQ_4:24, NAT_1:11
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h2) /. nx) by Th7
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1)) by A51, A53, A54, A55, A56, FUNCT_1:23 ;
then A130: S₂[ 0 ] by A22, A29, A43, Def12;
A131: for k3 being Nat st S₂[k3] holds
S₂[k3 + 1]

proof

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

assume A133: ((k + 1) + 1) + (k3 + 1) <= len F ; :: thesis: (accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = (accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1))
A134: ((k + 1) + 1) + k3 < (((k + 1) + 1) + k3) + 1 by XREAL_1:31;
then A135: ((k + 1) + 1) + k3 < len F by A133, XXREAL_0:2;
A136: 1 <= (k + 1) + 1 by NAT_1:11;
A137: (k + 1) + 1 <= ((k + 1) + 1) + k3 by NAT_1:11;
then A138: 1 <= ((k + 1) + 1) + k3 by A136, XXREAL_0:2;
A139: 1 <= (((k + 1) + 1) + k3) + 1 by NAT_1:11;
A140: (k + 1) + 1 < (((k + 1) + 1) + k3) + 1 by A137, A134, XXREAL_0:2;
A141: (accum (F (*) h4)) /. (((k + 1) + 1) + k3) = (accum (F (*) h4)) . (((k + 1) + 1) + k3) by A135, A63, A43, A138, FINSEQ_4:24;
(((k + 1) + 1) + k3) + 1 in Seg (len (F (*) h2)) by A47, A133, A139, FINSEQ_1:3;
then A142: (((k + 1) + 1) + k3) + 1 in dom (F (*) h2) by FINSEQ_1:def 3;
then A143: (F (*) h4) . ((((k + 1) + 1) + k3) + 1) = F . (h4 . ((((k + 1) + 1) + k3) + 1)) by A42, A45, FUNCT_1:22
.= F . (h2b /. ((((k + 1) + 1) + k3) + 1)) by A36, A37, A133, FINSEQ_4:24, NAT_1:11
.= F . (h2r /. ((((k + 1) + 1) + k3) + 1)) by A36, A50, A133, A140, FINSEQ_7:32, NAT_1:11
.= F . (h2r . ((((k + 1) + 1) + k3) + 1)) by A36, A133, FINSEQ_4:24, NAT_1:11
.= (F (*) h2) . ((((k + 1) + 1) + k3) + 1) by A142, FUNCT_1:22 ;
A144: (F (*) h4) /. ((((k + 1) + 1) + k3) + 1) = (F (*) h4) . ((((k + 1) + 1) + k3) + 1) by A43, A133, FINSEQ_4:24, NAT_1:11;
(accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = ((accum (F (*) h2)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1)) by Def12, A138, A135, A48
.= ((accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1)) by A48, A64, A132, A135, A138, A141, FINSEQ_4:24
.= ((accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h4) /. ((((k + 1) + 1) + k3) + 1)) by A48, A133, A143, A144, FINSEQ_4:24, NAT_1:11 ;
hence (accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1)) = (accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1)) by Def12, A138, A135, A43; :: thesis: verum

end;

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

end;

A145: for k3 being Nat holds S₂[k3] from NAT_1:sch 2(A130, A131);
((k + 1) + 1) + (i -' ((k + 1) + 1)) = (i - ((k + 1) + 1)) + ((k + 1) + 1) by A126, XREAL_1:235
.= i ;
hence (accum (F (*) h2)) . i = (accum (F (*) h4)) . i by A126, A145; :: thesis: verum

end;

rng h4 c= dom F ;
then A146: dom (F (*) h4) = dom h4 by RELAT_1:46;
then A147: Seg (len (F (*) h4)) = dom h4 by FINSEQ_1:def 3;
Seg (len (F (*) h4)) = dom F by A57, A146, FINSEQ_1:def 3;
then A148: len (F (*) h4) = len F by FINSEQ_1:def 3;
A149: ( 1 <= k + 1 & k + 1 < len (F (*) h4) ) by A22, A57, A147, FINSEQ_1:def 3, NAT_1:11;
A150: (F (*) h4) /. ((k + 1) + 1) = (F (*) h4) . ((k + 1) + 1) by A30, A25, A148, FINSEQ_4:24;
A151: F /. ((k + 1) + 1) = F . ((k + 1) + 1) by A30, A25, FINSEQ_4:24;
len (accum (F (*) h4)) = len (F (*) h4) by Def12;
then A152: (accum (F (*) h4)) /. (k + 1) = (accum (F (*) h4)) . (k + 1) by A149, FINSEQ_4:24;
A153: gF /. (k + 1) = gF . (k + 1) by A3, A22, A29, FINSEQ_4:24;
gF . ((k + 1) + 1) = (gF /. (k + 1)) + (F /. ((k + 1) + 1)) by A3, A22, A29
.= ((accum (F (*) h4)) /. (k + 1)) + (F /. ((k + 1) + 1)) by A21, A28, A58, A152, A153
.= ((accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1)) by A51, A53, A150, A151, FUNCT_1:23
.= (accum (F (*) h4)) . ((k + 1) + 1) by A149, Def12 ;
hence gF . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) by A25, A125; :: thesis: verum

end;

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

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

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

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

A156: ( 1 <= k + 1 & k + 1 < len (F (*) h2) ) by A22, A46, FINSEQ_1:def 3, NAT_1:11;
A157: F /. ((k + 1) + 1) = F . ((k + 1) + 1) by A30, A25, FINSEQ_4:24;
A158: 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 A159: ( k + 1 < i & i <= len F ) ; :: thesis: h2 . i = i
then A160: (k + 1) + 1 <= i by NAT_1:13;

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

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

hence h2 . i = i by A22, A159; :: thesis: verum

end;

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

hence h2 . i = i by A32, A155; :: thesis: verum

end;

end;

end;

len (accum (F (*) h2)) = len (F (*) h2) by Def12;
then A161: (accum (F (*) h2)) /. (k + 1) = (accum (F (*) h2)) . (k + 1) by A27, A48, FINSEQ_4:24, NAT_1:11;
A162: gF /. (k + 1) = gF . (k + 1) by A3, A48, A156, FINSEQ_4:24;
A163: F . ((k + 1) + 1) = (F (*) h2) . nx by A32, FUNCT_1:23;
gF . ((k + 1) + 1) = (gF /. (k + 1)) + (F /. ((k + 1) + 1)) by A3, A22, A156
.= ((accum (F (*) h2)) /. (k + 1)) + (F /. ((k + 1) + 1)) by A21, A28, A158, A161, A162
.= ((accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1)) by A25, A30, A48, A155, A157, A163, FINSEQ_4:24
.= (accum (F (*) h2)) . ((k + 1) + 1) by A156, Def12 ;
hence gF . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) ; :: thesis: verum

end;

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

hence gF . ((k + 1) + 1) = (accum (F (*) h2)) . ((k + 1) + 1) by A22, A32, A34; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

A164: for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A20);
A165: (len F) -' 1 = (len F) - 1 by A4, XREAL_1:235;
then for i being Nat st ((len F) -' 1) + 1 < i & i <= len F holds
h . i = i ;
then gF . (len F) = (accum (F (*) h)) . (len F) by A164, A165, XREAL_1:46
.= (accum F2) . (len F2) by A1, A11, FINSEQ_1:def 3
.= Sum F2 by A12, Th24 ;
hence Sum F2 = Sum F by A3; :: thesis: verum

end;

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

then A167: len F = 0 ;
A168: Sum F = 0* n by A166, Def11;
rng h c= dom F ;
then A169: dom (F (*) h) = dom h by RELAT_1:46;
dom F = {} by A167, FINSEQ_1:4, FINSEQ_1:def 3;
then Seg (len F) = dom F2 by A1, A169, FINSEQ_1:def 3;
then len F = len F2 by FINSEQ_1:def 3;
hence Sum F2 = Sum F by A166, A168, Def11; :: thesis: verum

end;

end;