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 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 ]
proof
let F, G be FinSequence of ExtREAL ; :: thesis: for s being Permutation of () st len F = 0 & G = F * s & not -infty in rng F holds
Sum F = Sum G

let s be Permutation of (); :: 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;
A4: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
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 ;
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 ;
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 ;
then A14: F . (s . (n + 1)) = F . (p2 . (n + 1)) by ;
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 ;
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
.= F by ;
len s9 = n + 1 by ;
then A20: len G = n + 1 by ;
then A21: dom G = Seg (n + 1) by FINSEQ_1:def 3;
then A22: G . (n + 1) = F . (s . (n + 1)) by ;
reconsider p1 = p * (s9 | n) as Permutation of (Seg n) by ;
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 ;
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 ;
then A26: dom H = Seg (n + 1) by FINSEQ_1:def 3;
A27: len (H | n) = n by ;
A28: G | n = (H | n) * p1
proof
dom (H | n) = Seg n by ;
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 ;
then A30: len H1 = n by ;
A31: 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 that
A32: 1 <= i and
A33: i <= n ; :: thesis: (G | n) . i = ((H | n) * p1) . i
A34: i in Seg n by ;
then A35: s . i in rng s by ;
i in dom H1 by ;
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 ;
then reconsider a = p1 . i as Element of NAT ;
a <= n by ;
then A38: ((H | n) * p1) . i = H . (p1 . i) by ;
(s9 | n) . i = s . i by ;
then A39: p1 . i = p . (s . i) by ;
A40: (G | n) . i = G . i by ;
H . (p1 . i) = F . (p2 . (p1 . i)) by ;
then ((H | n) * p1) . i = F . (s . i) by ;
hence (G | n) . i = ((H | n) * p1) . i by ; :: thesis: verum
end;
len (G | n) = n by ;
hence G | n = (H | n) * p1 by ; :: thesis: verum
end;
G | n = G | (Seg n) by FINSEQ_1:def 15;
then G = (G | n) ^ <*(G . (n + 1))*> by ;
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 ;
then A43: Sum H = (Sum (H | n)) + (H . (n + 1)) by Lm1;
rng (H | n) c= rng H by ;
then not -infty in rng (H | n) by ;
then A44: Sum (G | n) = Sum (H | n) by A5, A27, A28;
H . (n + 1) = F . (p2 . (n + 1)) by ;
hence Sum F = Sum G by A11, A12, A25, A44, A14, A22, A41, A43, A24, A19, Lm5; :: thesis: verum
end;
end;
A45: 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 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 ;
then F is Function of (Seg 1),ExtREAL by FINSEQ_2:26;
then len G = 1 by ;
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 ;
A51: F = <*(F . 1)*> by ;
then rng F = {(F . 1)} by FINSEQ_1:39;
hence ( -infty in rng F or Sum F = Sum G ) by ; :: thesis: verum
end;
A52: for n being non zero Nat holds S1[n] from ( len F = 0 or len F <> 0 ) ;
then A53: S1[ len F] by ;
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 ; :: thesis: verum