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 ;
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 ;
then A11: q -' 1 <= (n + 1) - 1 by ;
A12: dom H = Seg (n + 1) by ;
then H is Function of (Seg (n + 1)),ExtREAL by FINSEQ_2:26;
then A13: len F = n + 1 by ;
then A14: len (F /^ q) = (n + 1) - q by ;
A15: n <= n + 1 by NAT_1:11;
then A16: len (F | (q -' 1)) = q -' 1 by ;
A17: dom F = Seg (n + 1) by ;
A18: for i being Nat st 1 <= i & i <= q -' 1 holds
(F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i
proof
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 ;
A22: (H | n) . i = H . i by ;
A23: ((H | n) | (q -' 1)) . i = (H | n) . i by ;
A24: i < (q -' 1) + 1 by ;
i <= n by ;
then i <= n + 1 by ;
then A25: i in Seg (n + 1) by ;
then F . i = H . (p . i) by ;
hence (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i by A5, A7, A21, A23, A22, A25, A24; :: thesis: verum
end;
0 + n <= 1 + n by XREAL_1:6;
then A26: len (H | n) = n by ;
then A27: len ((H | n) | (q -' 1)) = q -' 1 by ;
A28: len ((H | n) /^ (q -' 1)) = n - (q - 1) by ;
for i being Nat st 1 <= i & i <= (n + 1) - q holds
(F /^ q) . i = ((H | n) /^ (q -' 1)) . i
proof
reconsider n1 = (n + 1) - q as Element of NAT by ;
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 ;
A32: i in Seg n1 by ;
then i in dom ((H | n) /^ (q -' 1)) by ;
then A33: ((H | n) /^ (q -' 1)) . i = (H | n) . (i + (q -' 1)) by ;
i + (q -' 1) = (i + q) - 1 by A7;
then i + (q -' 1) <= n by ;
then A34: ((H | n) /^ (q -' 1)) . i = H . ((i + q) - 1) by ;
A35: 1 <= i + q by ;
then i + q in dom F by ;
then A36: F . (i + q) = H . (p . (i + q)) by ;
dom (F /^ q) = Seg n1 by ;
then A37: (F /^ q) . i = F . (i + q) by ;
i + q >= 1 + q by ;
then A38: i + q > q by NAT_1:13;
i + q in Seg (n + 1) by ;
hence (F /^ q) . i = ((H | n) /^ (q -' 1)) . i by A5, A37, A34, A36, A38; :: thesis: verum
end;
then A39: F /^ q = (H | n) /^ (q -' 1) by ;
A40: F = ((F | (q -' 1)) ^ <*(F . q)*>) ^ (F /^ q) by ;
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 ;
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 ;
then A45: not -infty in rng ((H | n) | (q -' 1)) by XBOOLE_0:def 3;
A46: not -infty in rng F by ;
then A47: not -infty in rng ((F | (q -' 1)) ^ <*(F . q)*>) by ;
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 ;
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 ;
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 ;
then A54: H = (H | n) ^ <*(H . (n + 1))*> by ;
A55: not -infty in rng ((H | n) /^ (q -' 1)) by ;
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
.= ((Sum ((H | n) | (q -' 1))) + (Sum ((H | n) /^ (q -' 1)))) + (H . (n + 1)) by
.= (Sum (H | n)) + (H . (n + 1)) by A8, A45, A55, Th8
.= Sum H by ; :: thesis: verum