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[1]
proof
let F,
G be
FinSequence of
ExtREAL ;
:: thesis: 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);
:: thesis: ( len F = 1 & G = F * s & not -infty in rng F implies Sum F = Sum G )
assume that A2:
len F = 1
and A3:
G = F * s
;
:: thesis: ( -infty in rng F or Sum F = Sum G )
A4:
F = <*(F . 1)*>
by A2, FINSEQ_1:57;
then A5:
rng F = {(F . 1)}
by FINSEQ_1:56;
reconsider s1 =
s as
FinSequence of
Seg 1
by FINSEQ_2:28;
A7:
dom F = Seg 1
by A2, FINSEQ_1:def 3;
dom s = Seg 1
by FUNCT_2:def 1;
then A8:
len s1 = 1
by FINSEQ_1:def 3;
F is
Function of
(Seg 1),
ExtREAL
by A7, FINSEQ_2:30;
then
len G = 1
by A3, A8, FINSEQ_2:37;
then A9:
G = <*(G . 1)*>
by FINSEQ_1:57;
then
rng G = {(G . 1)}
by FINSEQ_1:56;
then
G . 1
in rng G
by TARSKI:def 1;
then
G . 1
in rng F
by A3, FUNCT_1:25;
hence
(
-infty in rng F or
Sum F = Sum G )
by A4, A5, A9, TARSKI:def 1;
:: thesis: verum
end;
A10:
for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non
empty Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A11:
S1[
n]
;
:: thesis: S1[n + 1]
thus
S1[
n + 1]
:: thesis: verumproof
let F,
G be
FinSequence of
ExtREAL ;
:: thesis: 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));
:: thesis: ( len F = n + 1 & G = F * s & not -infty in rng F implies Sum F = Sum G )
assume that A12:
len F = n + 1
and A13:
G = F * s
and A14:
not
-infty in rng F
;
:: thesis: Sum F = Sum G
A15:
dom F = Seg (n + 1)
by A12, FINSEQ_1:def 3;
A17:
(
dom s = Seg (n + 1) &
rng s = Seg (n + 1) )
by FUNCT_2:def 1, FUNCT_2:def 3;
reconsider s' =
s as
FinSequence of
Seg (n + 1) by FINSEQ_2:28;
A18:
len s' = n + 1
by A17, FINSEQ_1:def 3;
A19:
F is
Function of
(Seg (n + 1)),
ExtREAL
by A15, FINSEQ_2:30;
then A20:
len G = n + 1
by A13, A18, FINSEQ_2:37;
then A21:
dom G = Seg (n + 1)
by FINSEQ_1:def 3;
n + 1
in dom s
by A17, FINSEQ_1:6;
then A22:
s . (n + 1) in Seg (n + 1)
by A17, FUNCT_1:def 5;
then reconsider q =
s . (n + 1) as
Element of
NAT ;
consider p being
Permutation of
(Seg (n + 1)) such that A23:
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 A22, Lm9;
A24:
dom p = Seg (n + 1)
by FUNCT_2:def 1;
reconsider p2 =
p " as
FinSequence of
Seg (n + 1) by FINSEQ_2:28;
reconsider H =
F * p2 as
FinSequence of
ExtREAL by A19, FINSEQ_2:36;
dom p2 = rng p
by FUNCT_1:55;
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 A19, FINSEQ_2:37;
then A26:
dom H = Seg (n + 1)
by FINSEQ_1:def 3;
reconsider p1 =
p * (s' | n) as
Permutation of
(Seg n) by A23, Lm10;
A28:
dom p1 = Seg n
by FUNCT_2:def 1;
reconsider p1' =
p1 as
FinSequence of
Seg n by FINSEQ_2:28;
A29:
0 + n <= 1
+ n
by XREAL_1:8;
then A30:
Seg n c= Seg (n + 1)
by FINSEQ_1:7;
A31:
len (H | n) = n
by A25, A29, FINSEQ_1:80;
A32:
G | n = (H | n) * p1
proof
A33:
len (G | n) = n
by A20, A29, FINSEQ_1:80;
dom (H | n) = Seg n
by A31, FINSEQ_1:def 3;
then A34:
H | n is
Function of
(Seg n),
ExtREAL
by FINSEQ_2:30;
then reconsider H1 =
(H | n) * p1' as
FinSequence of
ExtREAL by FINSEQ_2:36;
n in NAT
by ORDINAL1:def 13;
then
len p1' = n
by A28, FINSEQ_1:def 3;
then A35:
len H1 = n
by A34, FINSEQ_2:37;
for
i being
Nat st 1
<= i &
i <= n holds
(G | n) . i = ((H | n) * p1) . i
proof
let i be
Nat;
:: thesis: ( 1 <= i & i <= n implies (G | n) . i = ((H | n) * p1) . i )
assume A36:
( 1
<= i &
i <= n )
;
:: thesis: (G | n) . i = ((H | n) * p1) . i
then A37:
(G | n) . i = G . i
by FINSEQ_3:121;
A38:
i in Seg n
by A36, FINSEQ_1:3;
then
i in dom H1
by A35, FINSEQ_1:def 3;
then A39:
((H | n) * p1) . i = (H | n) . (p1 . i)
by FUNCT_1:22;
(s' | n) . i = s . i
by A36, FINSEQ_3:121;
then A40:
p1 . i = p . (s . i)
by A28, A38, FUNCT_1:22;
rng p1 = Seg n
by FUNCT_2:def 3;
then A41:
p1 . i in Seg n
by A28, A38, FUNCT_1:12;
then reconsider a =
p1 . i as
Element of
NAT ;
a <= n
by A41, FINSEQ_1:3;
then A42:
((H | n) * p1) . i = H . (p1 . i)
by A39, FINSEQ_3:121;
A43:
H . (p1 . i) = F . (p2 . (p1 . i))
by A26, A30, A41, FUNCT_1:22;
s . i in rng s
by A17, A30, A38, FUNCT_1:12;
then
((H | n) * p1) . i = F . (s . i)
by A17, A24, A40, A42, A43, FUNCT_1:56;
hence
(G | n) . i = ((H | n) * p1) . i
by A13, A21, A30, A37, A38, FUNCT_1:22;
:: thesis: verum
end;
hence
G | n = (H | n) * p1
by A33, A35, FINSEQ_1:18;
:: thesis: verum
end;
A44:
H | n = H | (Seg n)
by FINSEQ_1:def 15;
then
rng (H | n) c= rng H
by RELAT_1:99;
then
not
-infty in rng (H | n)
by A14, FUNCT_1:25;
then A45:
Sum (G | n) = Sum (H | n)
by A11, A31, A32;
p . q = n + 1
by A22, A23;
then A46:
F . (s . (n + 1)) = F . (p2 . (n + 1))
by A22, A24, FUNCT_1:56;
A47:
(
H . (n + 1) = F . (p2 . (n + 1)) &
G . (n + 1) = F . (s . (n + 1)) )
by A13, A21, A26, FINSEQ_1:6, FUNCT_1:22;
G | n = G | (Seg n)
by FINSEQ_1:def 15;
then
(
G = (G | n) ^ <*(G . (n + 1))*> &
H = (H | n) ^ <*(H . (n + 1))*> )
by A20, A25, A44, FINSEQ_3:61;
then A48:
(
Sum G = (Sum (G | n)) + (G . (n + 1)) &
Sum H = (Sum (H | n)) + (H . (n + 1)) )
by Lm4;
A49:
not
-infty in rng H
by A14, FUNCT_1:25;
H * p =
F * (p2 * p)
by RELAT_1:55
.=
F * (id (Seg (n + 1)))
by A24, FUNCT_1:61
.=
F
by A15, RELAT_1:78
;
hence
Sum F = Sum G
by A22, A23, A25, A45, A46, A47, A48, A49, Lm11;
:: thesis: verum
end;
end;
A50:
for n being non empty Nat holds S1[n]
from NAT_1:sch 10(A1, A10);
A51:
S1[ 0 ]
let F, G be FinSequence of ExtREAL ; :: thesis: 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); :: thesis: ( G = F * s & not -infty in rng F implies Sum F = Sum G )
A54:
S1[ len F]
A55:
dom F = Seg (len F)
by FINSEQ_1:def 3;
assume
( G = F * s & not -infty in rng F )
; :: thesis: Sum F = Sum G
hence
Sum F = Sum G
by A54, A55; :: thesis: verum