let F, G be FinSequence of ExtREAL ; for s being Permutation of (dom F) st G = F * s & not -infty in rng F holds
Sum F = Sum G
let s be Permutation of (dom F); ( G = F * s & not -infty in rng F implies Sum F = Sum G )
defpred S1[ Nat] means for F, G being FinSequence of ExtREAL
for s being Permutation of (Seg $1) st len F = $1 & G = F * s & not -infty in rng F holds
Sum F = Sum G;
A1:
S1[ 0 ]
A4:
for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non
zero Nat;
( S1[n] implies S1[n + 1] )
assume A5:
S1[
n]
;
S1[n + 1]
thus
S1[
n + 1]
verumproof
let F,
G be
FinSequence of
ExtREAL ;
for s being Permutation of (Seg (n + 1)) st len F = n + 1 & G = F * s & not -infty in rng F holds
Sum F = Sum Glet s be
Permutation of
(Seg (n + 1));
( len F = n + 1 & G = F * s & not -infty in rng F implies Sum F = Sum G )
assume that A6:
len F = n + 1
and A7:
G = F * s
and A8:
not
-infty in rng F
;
Sum F = Sum G
reconsider s9 =
s as
FinSequence of
Seg (n + 1) by FINSEQ_2:25;
A9:
rng s = Seg (n + 1)
by FUNCT_2:def 3;
A10:
dom s = Seg (n + 1)
by FUNCT_2:def 1;
then
n + 1
in dom s
by FINSEQ_1:4;
then A11:
s . (n + 1) in Seg (n + 1)
by A9, FUNCT_1:def 3;
then reconsider q =
s . (n + 1) as
Element of
NAT ;
consider p being
Permutation of
(Seg (n + 1)) such that A12:
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 ) )
by A11, Lm3;
reconsider p2 =
p " as
FinSequence of
Seg (n + 1) by FINSEQ_2:25;
A13:
dom p = Seg (n + 1)
by FUNCT_2:def 1;
p . q = n + 1
by A11, A12;
then A14:
F . (s . (n + 1)) = F . (p2 . (n + 1))
by A11, A13, FUNCT_1:34;
A15:
0 + n <= 1
+ n
by XREAL_1:6;
then A16:
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
A17:
dom F = Seg (n + 1)
by A6, FINSEQ_1:def 3;
then A18:
F is
Function of
(Seg (n + 1)),
ExtREAL
by FINSEQ_2:26;
then reconsider H =
F * p2 as
FinSequence of
ExtREAL by FINSEQ_2:32;
A19:
H * p =
F * (p2 * p)
by RELAT_1:36
.=
F * (id (Seg (n + 1)))
by A13, FUNCT_1:39
.=
F
by A17, RELAT_1:52
;
len s9 = n + 1
by A10, FINSEQ_1:def 3;
then A20:
len G = n + 1
by A7, A18, FINSEQ_2:33;
then A21:
dom G = Seg (n + 1)
by FINSEQ_1:def 3;
then A22:
G . (n + 1) = F . (s . (n + 1))
by A7, FINSEQ_1:4, FUNCT_1:12;
reconsider p1 =
p * (s9 | n) as
Permutation of
(Seg n) by A12, Lm4;
A23:
dom p1 = Seg n
by FUNCT_2:def 1;
reconsider p19 =
p1 as
FinSequence of
Seg n by FINSEQ_2:25;
A24:
not
-infty in rng H
by A8, FUNCT_1:14;
dom p2 = rng p
by FUNCT_1:33;
then
dom p2 = Seg (n + 1)
by FUNCT_2:def 3;
then
len p2 = n + 1
by FINSEQ_1:def 3;
then A25:
len H = n + 1
by A18, FINSEQ_2:33;
then A26:
dom H = Seg (n + 1)
by FINSEQ_1:def 3;
A27:
len (H | n) = n
by A25, A15, FINSEQ_1:59;
A28:
G | n = (H | n) * p1
proof
dom (H | n) = Seg n
by A27, FINSEQ_1:def 3;
then A29:
H | n is
Function of
(Seg n),
ExtREAL
by FINSEQ_2:26;
then reconsider H1 =
(H | n) * p19 as
FinSequence of
ExtREAL by FINSEQ_2:32;
n in NAT
by ORDINAL1:def 12;
then
len p19 = n
by A23, FINSEQ_1:def 3;
then A30:
len H1 = n
by A29, FINSEQ_2:33;
A31:
for
i being
Nat st 1
<= i &
i <= n holds
(G | n) . i = ((H | n) * p1) . i
proof
let i be
Nat;
( 1 <= i & i <= n implies (G | n) . i = ((H | n) * p1) . i )
assume that A32:
1
<= i
and A33:
i <= n
;
(G | n) . i = ((H | n) * p1) . i
A34:
i in Seg n
by A32, A33, FINSEQ_1:1;
then A35:
s . i in rng s
by A10, A16, FUNCT_1:3;
i in dom H1
by A30, A34, FINSEQ_1:def 3;
then A36:
((H | n) * p1) . i = (H | n) . (p1 . i)
by FUNCT_1:12;
rng p1 = Seg n
by FUNCT_2:def 3;
then A37:
p1 . i in Seg n
by A23, A34, FUNCT_1:3;
then reconsider a =
p1 . i as
Element of
NAT ;
a <= n
by A37, FINSEQ_1:1;
then A38:
((H | n) * p1) . i = H . (p1 . i)
by A36, FINSEQ_3:112;
(s9 | n) . i = s . i
by A33, FINSEQ_3:112;
then A39:
p1 . i = p . (s . i)
by A23, A34, FUNCT_1:12;
A40:
(G | n) . i = G . i
by A33, FINSEQ_3:112;
H . (p1 . i) = F . (p2 . (p1 . i))
by A26, A16, A37, FUNCT_1:12;
then
((H | n) * p1) . i = F . (s . i)
by A13, A39, A38, A35, FUNCT_1:34;
hence
(G | n) . i = ((H | n) * p1) . i
by A7, A21, A16, A40, A34, FUNCT_1:12;
verum
end;
len (G | n) = n
by A20, A15, FINSEQ_1:59;
hence
G | n = (H | n) * p1
by A30, A31, FINSEQ_1:14;
verum
end;
G | n = G | (Seg n)
by FINSEQ_1:def 15;
then
G = (G | n) ^ <*(G . (n + 1))*>
by A20, FINSEQ_3:55;
then A41:
Sum G = (Sum (G | n)) + (G . (n + 1))
by Lm1;
A42:
H | n = H | (Seg n)
by FINSEQ_1:def 15;
then
H = (H | n) ^ <*(H . (n + 1))*>
by A25, FINSEQ_3:55;
then A43:
Sum H = (Sum (H | n)) + (H . (n + 1))
by Lm1;
rng (H | n) c= rng H
by A42, RELAT_1:70;
then
not
-infty in rng (H | n)
by A8, FUNCT_1:14;
then A44:
Sum (G | n) = Sum (H | n)
by A5, A27, A28;
H . (n + 1) = F . (p2 . (n + 1))
by A26, FINSEQ_1:4, FUNCT_1:12;
hence
Sum F = Sum G
by A11, A12, A25, A44, A14, A22, A41, A43, A24, A19, Lm5;
verum
end;
end;
A45:
S1[1]
proof
let F,
G be
FinSequence of
ExtREAL ;
for s being Permutation of (Seg 1) st len F = 1 & G = F * s & not -infty in rng F holds
Sum F = Sum Glet s be
Permutation of
(Seg 1);
( len F = 1 & G = F * s & not -infty in rng F implies Sum F = Sum G )
assume that A46:
len F = 1
and A47:
G = F * s
;
( -infty in rng F or Sum F = Sum G )
reconsider s1 =
s as
FinSequence of
Seg 1
by FINSEQ_2:25;
dom s = Seg 1
by FUNCT_2:def 1;
then A48:
len s1 = 1
by FINSEQ_1:def 3;
dom F = Seg 1
by A46, FINSEQ_1:def 3;
then
F is
Function of
(Seg 1),
ExtREAL
by FINSEQ_2:26;
then
len G = 1
by A47, A48, FINSEQ_2:33;
then A49:
G = <*(G . 1)*>
by FINSEQ_1:40;
then
rng G = {(G . 1)}
by FINSEQ_1:39;
then
G . 1
in rng G
by TARSKI:def 1;
then A50:
G . 1
in rng F
by A47, FUNCT_1:14;
A51:
F = <*(F . 1)*>
by A46, FINSEQ_1:40;
then
rng F = {(F . 1)}
by FINSEQ_1:39;
hence
(
-infty in rng F or
Sum F = Sum G )
by A51, A49, A50, TARSKI:def 1;
verum
end;
A52:
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(A45, A4);
( len F = 0 or len F <> 0 )
;
then A53:
S1[ len F]
by A1, A52;
assume that
A54:
G = F * s
and
A55:
not -infty in rng F
; Sum F = Sum G
dom F = Seg (len F)
by FINSEQ_1:def 3;
hence
Sum F = Sum G
by A53, A54, A55; verum