let n, q be Nat; :: thesis: for p being Permutation of (Seg (n + 1))

for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds

Sum F = Sum H

let p be Permutation of (Seg (n + 1)); :: thesis: for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds

Sum F = Sum H

let F, H be FinSequence of ExtREAL ; :: thesis: ( F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) implies Sum F = Sum H )

assume that

A1: F = H * p and

A2: q in Seg (n + 1) and

A3: len H = n + 1 and

A4: not -infty in rng H and

A5: for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ; :: thesis: Sum F = Sum H

A6: 1 <= q by A2, FINSEQ_1:1;

then q - 1 >= 1 - 1 by XREAL_1:9;

then A7: q -' 1 = q - 1 by XREAL_0:def 2;

set H1 = H | n;

A8: H | n = ((H | n) | (q -' 1)) ^ ((H | n) /^ (q -' 1)) by RFINSEQ:8;

reconsider p9 = p as FinSequence of Seg (n + 1) by FINSEQ_2:25;

dom p = Seg (n + 1) by FUNCT_2:def 1;

then A9: len p9 = n + 1 by FINSEQ_1:def 3;

A10: q <= n + 1 by A2, FINSEQ_1:1;

then A11: q -' 1 <= (n + 1) - 1 by A7, XREAL_1:9;

A12: dom H = Seg (n + 1) by A3, FINSEQ_1:def 3;

then H is Function of (Seg (n + 1)),ExtREAL by FINSEQ_2:26;

then A13: len F = n + 1 by A1, A9, FINSEQ_2:33;

then A14: len (F /^ q) = (n + 1) - q by A10, RFINSEQ:def 1;

A15: n <= n + 1 by NAT_1:11;

then A16: len (F | (q -' 1)) = q -' 1 by A11, A13, FINSEQ_1:59, XXREAL_0:2;

A17: dom F = Seg (n + 1) by A13, FINSEQ_1:def 3;

A18: for i being Nat st 1 <= i & i <= q -' 1 holds

(F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i

then A26: len (H | n) = n by A3, FINSEQ_1:59;

then A27: len ((H | n) | (q -' 1)) = q -' 1 by A11, FINSEQ_1:59;

A28: len ((H | n) /^ (q -' 1)) = n - (q - 1) by A7, A11, A26, RFINSEQ:def 1;

for i being Nat st 1 <= i & i <= (n + 1) - q holds

(F /^ q) . i = ((H | n) /^ (q -' 1)) . i

A40: F = ((F | (q -' 1)) ^ <*(F . q)*>) ^ (F /^ q) by A6, A10, A13, FINSEQ_5:84;

then A41: rng F = (rng ((F | (q -' 1)) ^ <*(F . q)*>)) \/ (rng (F /^ q)) by FINSEQ_1:31;

p . q = n + 1 by A2, A5;

then A42: F . q = H . (n + 1) by A1, A2, A17, FUNCT_1:12;

A43: H | n = H | (Seg n) by FINSEQ_1:def 15;

then rng (H | n) c= rng H by RELAT_1:70;

then not -infty in rng (H | n) by A4;

then A44: not -infty in (rng ((H | n) | (q -' 1))) \/ (rng ((H | n) /^ (q -' 1))) by A8, FINSEQ_1:31;

then A45: not -infty in rng ((H | n) | (q -' 1)) by XBOOLE_0:def 3;

A46: not -infty in rng F by A1, A4, FUNCT_1:14;

then A47: not -infty in rng ((F | (q -' 1)) ^ <*(F . q)*>) by A41, XBOOLE_0:def 3;

then A48: not -infty in (rng (F | (q -' 1))) \/ (rng <*(F . q)*>) by FINSEQ_1:31;

then not -infty in rng (F | (q -' 1)) by XBOOLE_0:def 3;

then A49: Sum (F | (q -' 1)) <> -infty by Lm2;

not -infty in rng <*(F . q)*> by A48, XBOOLE_0:def 3;

then not -infty in {(F . q)} by FINSEQ_1:39;

then A50: -infty <> F . q by TARSKI:def 1;

A51: not -infty in rng (F /^ q) by A46, A41, XBOOLE_0:def 3;

then A52: Sum (F /^ q) <> -infty by Lm2;

A53: H | (n + 1) = H | (Seg (n + 1)) by FINSEQ_1:def 15;

H | (n + 1) = H by A3, FINSEQ_1:58;

then A54: H = (H | n) ^ <*(H . (n + 1))*> by A12, A43, A53, FINSEQ_1:4, FINSEQ_5:10;

A55: not -infty in rng ((H | n) /^ (q -' 1)) by A44, XBOOLE_0:def 3;

thus Sum F = (Sum ((F | (q -' 1)) ^ <*(F . q)*>)) + (Sum (F /^ q)) by A40, A47, A51, Th8

.= ((Sum (F | (q -' 1))) + (F . q)) + (Sum (F /^ q)) by Lm1

.= ((Sum (F | (q -' 1))) + (Sum (F /^ q))) + (F . q) by A50, A49, A52, XXREAL_3:29

.= ((Sum ((H | n) | (q -' 1))) + (Sum ((H | n) /^ (q -' 1)))) + (H . (n + 1)) by A16, A27, A18, A42, A39, FINSEQ_1:14

.= (Sum (H | n)) + (H . (n + 1)) by A8, A45, A55, Th8

.= Sum H by A54, Lm1 ; :: thesis: verum

for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds

Sum F = Sum H

let p be Permutation of (Seg (n + 1)); :: thesis: for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds

Sum F = Sum H

let F, H be FinSequence of ExtREAL ; :: thesis: ( F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) implies Sum F = Sum H )

assume that

A1: F = H * p and

A2: q in Seg (n + 1) and

A3: len H = n + 1 and

A4: not -infty in rng H and

A5: for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ; :: thesis: Sum F = Sum H

A6: 1 <= q by A2, FINSEQ_1:1;

then q - 1 >= 1 - 1 by XREAL_1:9;

then A7: q -' 1 = q - 1 by XREAL_0:def 2;

set H1 = H | n;

A8: H | n = ((H | n) | (q -' 1)) ^ ((H | n) /^ (q -' 1)) by RFINSEQ:8;

reconsider p9 = p as FinSequence of Seg (n + 1) by FINSEQ_2:25;

dom p = Seg (n + 1) by FUNCT_2:def 1;

then A9: len p9 = n + 1 by FINSEQ_1:def 3;

A10: q <= n + 1 by A2, FINSEQ_1:1;

then A11: q -' 1 <= (n + 1) - 1 by A7, XREAL_1:9;

A12: dom H = Seg (n + 1) by A3, FINSEQ_1:def 3;

then H is Function of (Seg (n + 1)),ExtREAL by FINSEQ_2:26;

then A13: len F = n + 1 by A1, A9, FINSEQ_2:33;

then A14: len (F /^ q) = (n + 1) - q by A10, RFINSEQ:def 1;

A15: n <= n + 1 by NAT_1:11;

then A16: len (F | (q -' 1)) = q -' 1 by A11, A13, FINSEQ_1:59, XXREAL_0:2;

A17: dom F = Seg (n + 1) by A13, FINSEQ_1:def 3;

A18: for i being Nat st 1 <= i & i <= q -' 1 holds

(F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i

proof

0 + n <= 1 + n
by XREAL_1:6;
let i be Nat; :: thesis: ( 1 <= i & i <= q -' 1 implies (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i )

assume that

A19: 1 <= i and

A20: i <= q -' 1 ; :: thesis: (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i

A21: (F | (q -' 1)) . i = F . i by A20, FINSEQ_3:112;

A22: (H | n) . i = H . i by A11, A20, FINSEQ_3:112, XXREAL_0:2;

A23: ((H | n) | (q -' 1)) . i = (H | n) . i by A20, FINSEQ_3:112;

A24: i < (q -' 1) + 1 by A20, NAT_1:13;

i <= n by A11, A20, XXREAL_0:2;

then i <= n + 1 by A15, XXREAL_0:2;

then A25: i in Seg (n + 1) by A19, FINSEQ_1:1;

then F . i = H . (p . i) by A1, A17, FUNCT_1:12;

hence (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i by A5, A7, A21, A23, A22, A25, A24; :: thesis: verum

end;assume that

A19: 1 <= i and

A20: i <= q -' 1 ; :: thesis: (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i

A21: (F | (q -' 1)) . i = F . i by A20, FINSEQ_3:112;

A22: (H | n) . i = H . i by A11, A20, FINSEQ_3:112, XXREAL_0:2;

A23: ((H | n) | (q -' 1)) . i = (H | n) . i by A20, FINSEQ_3:112;

A24: i < (q -' 1) + 1 by A20, NAT_1:13;

i <= n by A11, A20, XXREAL_0:2;

then i <= n + 1 by A15, XXREAL_0:2;

then A25: i in Seg (n + 1) by A19, FINSEQ_1:1;

then F . i = H . (p . i) by A1, A17, FUNCT_1:12;

hence (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i by A5, A7, A21, A23, A22, A25, A24; :: thesis: verum

then A26: len (H | n) = n by A3, FINSEQ_1:59;

then A27: len ((H | n) | (q -' 1)) = q -' 1 by A11, FINSEQ_1:59;

A28: len ((H | n) /^ (q -' 1)) = n - (q - 1) by A7, A11, A26, RFINSEQ:def 1;

for i being Nat st 1 <= i & i <= (n + 1) - q holds

(F /^ q) . i = ((H | n) /^ (q -' 1)) . i

proof

then A39:
F /^ q = (H | n) /^ (q -' 1)
by A14, A28, FINSEQ_1:14;
reconsider n1 = (n + 1) - q as Element of NAT by A10, INT_1:5;

let i be Nat; :: thesis: ( 1 <= i & i <= (n + 1) - q implies (F /^ q) . i = ((H | n) /^ (q -' 1)) . i )

assume that

A29: 1 <= i and

A30: i <= (n + 1) - q ; :: thesis: (F /^ q) . i = ((H | n) /^ (q -' 1)) . i

A31: i + q <= n + 1 by A30, XREAL_1:19;

A32: i in Seg n1 by A29, A30, FINSEQ_1:1;

then i in dom ((H | n) /^ (q -' 1)) by A28, FINSEQ_1:def 3;

then A33: ((H | n) /^ (q -' 1)) . i = (H | n) . (i + (q -' 1)) by A11, A26, RFINSEQ:def 1;

i + (q -' 1) = (i + q) - 1 by A7;

then i + (q -' 1) <= n by A31, XREAL_1:20;

then A34: ((H | n) /^ (q -' 1)) . i = H . ((i + q) - 1) by A7, A33, FINSEQ_3:112;

A35: 1 <= i + q by A29, NAT_1:12;

then i + q in dom F by A17, A31, FINSEQ_1:1;

then A36: F . (i + q) = H . (p . (i + q)) by A1, FUNCT_1:12;

dom (F /^ q) = Seg n1 by A14, FINSEQ_1:def 3;

then A37: (F /^ q) . i = F . (i + q) by A10, A13, A32, RFINSEQ:def 1;

i + q >= 1 + q by A29, XREAL_1:6;

then A38: i + q > q by NAT_1:13;

i + q in Seg (n + 1) by A31, A35, FINSEQ_1:1;

hence (F /^ q) . i = ((H | n) /^ (q -' 1)) . i by A5, A37, A34, A36, A38; :: thesis: verum

end;let i be Nat; :: thesis: ( 1 <= i & i <= (n + 1) - q implies (F /^ q) . i = ((H | n) /^ (q -' 1)) . i )

assume that

A29: 1 <= i and

A30: i <= (n + 1) - q ; :: thesis: (F /^ q) . i = ((H | n) /^ (q -' 1)) . i

A31: i + q <= n + 1 by A30, XREAL_1:19;

A32: i in Seg n1 by A29, A30, FINSEQ_1:1;

then i in dom ((H | n) /^ (q -' 1)) by A28, FINSEQ_1:def 3;

then A33: ((H | n) /^ (q -' 1)) . i = (H | n) . (i + (q -' 1)) by A11, A26, RFINSEQ:def 1;

i + (q -' 1) = (i + q) - 1 by A7;

then i + (q -' 1) <= n by A31, XREAL_1:20;

then A34: ((H | n) /^ (q -' 1)) . i = H . ((i + q) - 1) by A7, A33, FINSEQ_3:112;

A35: 1 <= i + q by A29, NAT_1:12;

then i + q in dom F by A17, A31, FINSEQ_1:1;

then A36: F . (i + q) = H . (p . (i + q)) by A1, FUNCT_1:12;

dom (F /^ q) = Seg n1 by A14, FINSEQ_1:def 3;

then A37: (F /^ q) . i = F . (i + q) by A10, A13, A32, RFINSEQ:def 1;

i + q >= 1 + q by A29, XREAL_1:6;

then A38: i + q > q by NAT_1:13;

i + q in Seg (n + 1) by A31, A35, FINSEQ_1:1;

hence (F /^ q) . i = ((H | n) /^ (q -' 1)) . i by A5, A37, A34, A36, A38; :: thesis: verum

A40: F = ((F | (q -' 1)) ^ <*(F . q)*>) ^ (F /^ q) by A6, A10, A13, FINSEQ_5:84;

then A41: rng F = (rng ((F | (q -' 1)) ^ <*(F . q)*>)) \/ (rng (F /^ q)) by FINSEQ_1:31;

p . q = n + 1 by A2, A5;

then A42: F . q = H . (n + 1) by A1, A2, A17, FUNCT_1:12;

A43: H | n = H | (Seg n) by FINSEQ_1:def 15;

then rng (H | n) c= rng H by RELAT_1:70;

then not -infty in rng (H | n) by A4;

then A44: not -infty in (rng ((H | n) | (q -' 1))) \/ (rng ((H | n) /^ (q -' 1))) by A8, FINSEQ_1:31;

then A45: not -infty in rng ((H | n) | (q -' 1)) by XBOOLE_0:def 3;

A46: not -infty in rng F by A1, A4, FUNCT_1:14;

then A47: not -infty in rng ((F | (q -' 1)) ^ <*(F . q)*>) by A41, XBOOLE_0:def 3;

then A48: not -infty in (rng (F | (q -' 1))) \/ (rng <*(F . q)*>) by FINSEQ_1:31;

then not -infty in rng (F | (q -' 1)) by XBOOLE_0:def 3;

then A49: Sum (F | (q -' 1)) <> -infty by Lm2;

not -infty in rng <*(F . q)*> by A48, XBOOLE_0:def 3;

then not -infty in {(F . q)} by FINSEQ_1:39;

then A50: -infty <> F . q by TARSKI:def 1;

A51: not -infty in rng (F /^ q) by A46, A41, XBOOLE_0:def 3;

then A52: Sum (F /^ q) <> -infty by Lm2;

A53: H | (n + 1) = H | (Seg (n + 1)) by FINSEQ_1:def 15;

H | (n + 1) = H by A3, FINSEQ_1:58;

then A54: H = (H | n) ^ <*(H . (n + 1))*> by A12, A43, A53, FINSEQ_1:4, FINSEQ_5:10;

A55: not -infty in rng ((H | n) /^ (q -' 1)) by A44, XBOOLE_0:def 3;

thus Sum F = (Sum ((F | (q -' 1)) ^ <*(F . q)*>)) + (Sum (F /^ q)) by A40, A47, A51, Th8

.= ((Sum (F | (q -' 1))) + (F . q)) + (Sum (F /^ q)) by Lm1

.= ((Sum (F | (q -' 1))) + (Sum (F /^ q))) + (F . q) by A50, A49, A52, XXREAL_3:29

.= ((Sum ((H | n) | (q -' 1))) + (Sum ((H | n) /^ (q -' 1)))) + (H . (n + 1)) by A16, A27, A18, A42, A39, FINSEQ_1:14

.= (Sum (H | n)) + (H . (n + 1)) by A8, A45, A55, Th8

.= Sum H by A54, Lm1 ; :: thesis: verum