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 & q <= n + 1 )
by A2, FINSEQ_1:3;
then
q - 1 >= 1 - 1
by XREAL_1:11;
then A7:
q -' 1 = q - 1
by XREAL_0:def 2;
then A8:
q -' 1 <= (n + 1) - 1
by A6, XREAL_1:11;
A9:
n <= n + 1
by NAT_1:11;
A11:
dom p = Seg (n + 1)
by FUNCT_2:def 1;
reconsider p' = p as FinSequence of Seg (n + 1) by FINSEQ_2:28;
A12:
len p' = n + 1
by A11, FINSEQ_1:def 3;
A13:
dom H = Seg (n + 1)
by A3, FINSEQ_1:def 3;
then
H is Function of (Seg (n + 1)),ExtREAL
by FINSEQ_2:30;
then A14:
len F = n + 1
by A1, A12, FINSEQ_2:37;
then A15:
dom F = Seg (n + 1)
by FINSEQ_1:def 3;
set H1 = H | n;
0 + n <= 1 + n
by XREAL_1:8;
then A16:
len (H | n) = n
by A3, FINSEQ_1:80;
then A17:
( len (F | (q -' 1)) = q -' 1 & len ((H | n) | (q -' 1)) = q -' 1 )
by A8, A9, A14, FINSEQ_1:80, XXREAL_0:2;
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 A19:
( 1
<= i &
i <= q -' 1 )
;
:: thesis: (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i
then A20:
(
(F | (q -' 1)) . i = F . i &
((H | n) | (q -' 1)) . i = (H | n) . i )
by FINSEQ_3:121;
A21:
i <= n
by A8, A19, XXREAL_0:2;
A22:
(H | n) . i = H . i
by A8, A19, FINSEQ_3:121, XXREAL_0:2;
i <= n + 1
by A9, A21, XXREAL_0:2;
then A23:
i in Seg (n + 1)
by A19, FINSEQ_1:3;
then A24:
F . i = H . (p . i)
by A1, A15, FUNCT_1:22;
i < (q -' 1) + 1
by A19, NAT_1:13;
hence
(F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i
by A5, A7, A20, A22, A23, A24;
:: thesis: verum
end;
p . q = n + 1
by A2, A5;
then A25:
F . q = H . (n + 1)
by A1, A2, A15, FUNCT_1:22;
A26:
len (F /^ q) = (n + 1) - q
by A6, A14, RFINSEQ:def 2;
A27:
len ((H | n) /^ (q -' 1)) = n - (q - 1)
by A7, A8, A16, RFINSEQ:def 2;
for i being Nat st 1 <= i & i <= (n + 1) - q holds
(F /^ q) . i = ((H | n) /^ (q -' 1)) . i
proof
let i be
Nat;
:: thesis: ( 1 <= i & i <= (n + 1) - q implies (F /^ q) . i = ((H | n) /^ (q -' 1)) . i )
assume A28:
( 1
<= i &
i <= (n + 1) - q )
;
:: thesis: (F /^ q) . i = ((H | n) /^ (q -' 1)) . i
reconsider n1 =
(n + 1) - q as
Element of
NAT by A6, INT_1:18;
A29:
i in Seg n1
by A28, FINSEQ_1:3;
dom (F /^ q) = Seg n1
by A26, FINSEQ_1:def 3;
then A30:
(F /^ q) . i = F . (i + q)
by A6, A14, A29, RFINSEQ:def 2;
i in dom ((H | n) /^ (q -' 1))
by A27, A29, FINSEQ_1:def 3;
then A31:
((H | n) /^ (q -' 1)) . i = (H | n) . (i + (q -' 1))
by A8, A16, RFINSEQ:def 2;
A32:
i + (q -' 1) = (i + q) - 1
by A7;
A33:
i + q <= n + 1
by A28, XREAL_1:21;
then
i + (q -' 1) <= n
by A32, XREAL_1:22;
then A34:
((H | n) /^ (q -' 1)) . i = H . ((i + q) - 1)
by A7, A31, FINSEQ_3:121;
1
<= i + q
by A28, NAT_1:12;
then A35:
(
i + q in Seg (n + 1) &
i + q in dom F )
by A15, A33, FINSEQ_1:3;
then A36:
F . (i + q) = H . (p . (i + q))
by A1, FUNCT_1:22;
i + q >= 1
+ q
by A28, XREAL_1:8;
then
i + q > q
by NAT_1:13;
hence
(F /^ q) . i = ((H | n) /^ (q -' 1)) . i
by A5, A30, A34, A35, A36;
:: thesis: verum
end;
then A37:
F /^ q = (H | n) /^ (q -' 1)
by A26, A27, FINSEQ_1:18;
A38:
not -infty in rng F
by A1, A4, FUNCT_1:25;
q in NAT
by ORDINAL1:def 13;
then A39:
F = ((F | (q -' 1)) ^ <*(F . q)*>) ^ (F /^ q)
by A6, A14, POLYNOM4:3;
then
rng F = (rng ((F | (q -' 1)) ^ <*(F . q)*>)) \/ (rng (F /^ q))
by FINSEQ_1:44;
then A40:
( not -infty in rng ((F | (q -' 1)) ^ <*(F . q)*>) & not -infty in rng (F /^ q) )
by A38, XBOOLE_0:def 3;
then
not -infty in (rng (F | (q -' 1))) \/ (rng <*(F . q)*>)
by FINSEQ_1:44;
then A41:
( not -infty in rng (F | (q -' 1)) & not -infty in rng <*(F . q)*> )
by XBOOLE_0:def 3;
then
not -infty in {(F . q)}
by FINSEQ_1:56;
then A42:
-infty <> F . q
by TARSKI:def 1;
A43:
( Sum (F | (q -' 1)) <> -infty & Sum (F /^ q) <> -infty )
by A40, A41, Lm5;
A44:
H | n = H | (Seg n)
by FINSEQ_1:def 15;
then
rng (H | n) c= rng H
by RELAT_1:99;
then A45:
not -infty in rng (H | n)
by A4;
A46:
H | n = ((H | n) | (q -' 1)) ^ ((H | n) /^ (q -' 1))
by RFINSEQ:21;
then
not -infty in (rng ((H | n) | (q -' 1))) \/ (rng ((H | n) /^ (q -' 1)))
by A45, FINSEQ_1:44;
then A47:
( not -infty in rng ((H | n) | (q -' 1)) & not -infty in rng ((H | n) /^ (q -' 1)) )
by XBOOLE_0:def 3;
( H | (n + 1) = H & H | (n + 1) = H | (Seg (n + 1)) )
by A3, FINSEQ_1:79, FINSEQ_1:def 15;
then A48:
H = (H | n) ^ <*(H . (n + 1))*>
by A13, A44, FINSEQ_1:6, FINSEQ_5:11;
thus Sum F =
(Sum ((F | (q -' 1)) ^ <*(F . q)*>)) + (Sum (F /^ q))
by A39, A40, Th7
.=
((Sum (F | (q -' 1))) + (F . q)) + (Sum (F /^ q))
by Lm4
.=
((Sum (F | (q -' 1))) + (Sum (F /^ q))) + (F . q)
by A42, A43, XXREAL_3:30
.=
((Sum ((H | n) | (q -' 1))) + (Sum ((H | n) /^ (q -' 1)))) + (H . (n + 1))
by A17, A18, A25, A37, FINSEQ_1:18
.=
(Sum (H | n)) + (H . (n + 1))
by A46, A47, Th7
.=
Sum H
by A48, Lm4
; :: thesis: verum