let n, q be Nat; 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)); 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 ; ( 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 ) )
; 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
let i be
Nat;
( 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
;
(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;
verum
end;
0 + n <= 1 + n
by XREAL_1:6;
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
reconsider n1 =
(n + 1) - q as
Element of
NAT by A10, INT_1:5;
let i be
Nat;
( 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
;
(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;
verum
end;
then A39:
F /^ q = (H | n) /^ (q -' 1)
by A14, A28, FINSEQ_1:14;
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
; verum