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 )

defpred S_{1}[ 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: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[1]
_{1}[n]
from NAT_1:sch 10(A45, A4);

( len F = 0 or len F <> 0 ) ;

then A53: S_{1}[ len F]
by A1, A52;

assume that

A54: G = F * s and

A55: not -infty in rng F ; :: thesis: Sum F = Sum G

dom F = Seg (len F) by FINSEQ_1:def 3;

hence Sum F = Sum G by A53, A54, A55; :: thesis: verum

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 )

defpred S

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: S

proof

A4:
for n being non zero Nat st S
let F, G be FinSequence of ExtREAL ; :: thesis: for s being Permutation of (Seg 0) st len F = 0 & G = F * s & not -infty in rng F holds

Sum F = Sum G

let s be Permutation of (Seg 0); :: thesis: ( len F = 0 & G = F * s & not -infty in rng F implies Sum F = Sum G )

assume that

A2: len F = 0 and

A3: G = F * s ; :: thesis: ( -infty in rng F or Sum F = Sum G )

F = <*> ExtREAL by A2;

hence ( -infty in rng F or Sum F = Sum G ) by A3; :: thesis: verum

end;Sum F = Sum G

let s be Permutation of (Seg 0); :: thesis: ( len F = 0 & G = F * s & not -infty in rng F implies Sum F = Sum G )

assume that

A2: len F = 0 and

A3: G = F * s ; :: thesis: ( -infty in rng F or Sum F = Sum G )

F = <*> ExtREAL by A2;

hence ( -infty in rng F or Sum F = Sum G ) by A3; :: thesis: verum

S

proof

A45:
S
let n be non zero Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A5: S

thus S

proof

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 G

let 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

A6: len F = n + 1 and

A7: G = F * s and

A8: not -infty in rng F ; :: thesis: 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

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; :: thesis: verum

end;Sum F = Sum G

let 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

A6: len F = n + 1 and

A7: G = F * s and

A8: not -infty in rng F ; :: thesis: 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

G | n = G | (Seg n)
by FINSEQ_1:def 15;
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

hence G | n = (H | n) * p1 by A30, A31, FINSEQ_1:14; :: thesis: verum

end;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

len (G | n) = n
by A20, A15, FINSEQ_1:59;
let i be Nat; :: thesis: ( 1 <= i & i <= n implies (G | n) . i = ((H | n) * p1) . i )

assume that

A32: 1 <= i and

A33: i <= n ; :: thesis: (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; :: thesis: verum

end;assume that

A32: 1 <= i and

A33: i <= n ; :: thesis: (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; :: thesis: verum

hence G | n = (H | n) * p1 by A30, A31, FINSEQ_1:14; :: thesis: verum

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; :: thesis: verum

proof

A52:
for n being non zero Nat holds S
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 G

let 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

A46: len F = 1 and

A47: G = F * s ; :: thesis: ( -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; :: thesis: verum

end;Sum F = Sum G

let 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

A46: len F = 1 and

A47: G = F * s ; :: thesis: ( -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; :: thesis: verum

( len F = 0 or len F <> 0 ) ;

then A53: S

assume that

A54: G = F * s and

A55: not -infty in rng F ; :: thesis: Sum F = Sum G

dom F = Seg (len F) by FINSEQ_1:def 3;

hence Sum F = Sum G by A53, A54, A55; :: thesis: verum