:: EXTREAL1 semantic presentation
begin
definition
let x, y be R_eal;
:: original: *
redefine funcx * y -> R_eal;
coherence
x * y is R_eal by XXREAL_0:def_1;
end;
theorem Th1: :: EXTREAL1:1
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x * y = a * b by XXREAL_3:def_5;
definition
let x, y be R_eal;
:: original: /
redefine funcx / y -> R_eal;
coherence
x / y is R_eal by XXREAL_0:def_1;
end;
theorem Th2: :: EXTREAL1:2
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x / y = a / b
proof
let x, y be R_eal; ::_thesis: for a, b being Real st x = a & y = b holds
x / y = a / b
let a, b be Real; ::_thesis: ( x = a & y = b implies x / y = a / b )
assume A1: ( x = a & y = b ) ; ::_thesis: x / y = a / b
reconsider a = a, b = b as real number ;
consider c being complex number such that
A2: y = c and
A3: y " = c " by A1, XXREAL_3:def_6;
x / y = x * (y ")
.= a * (c ") by A1, A3, XXREAL_3:def_5
.= a / b by A1, A2 ;
hence x / y = a / b ; ::_thesis: verum
end;
definition
let x be R_eal;
func|.x.| -> R_eal equals :Def1: :: EXTREAL1:def 1
x if 0 <= x
otherwise - x;
coherence
( ( 0 <= x implies x is R_eal ) & ( not 0 <= x implies - x is R_eal ) ) ;
consistency
for b1 being R_eal holds verum ;
projectivity
for b1, b2 being R_eal st ( 0 <= b2 implies b1 = b2 ) & ( not 0 <= b2 implies b1 = - b2 ) holds
( ( 0 <= b1 implies b1 = b1 ) & ( not 0 <= b1 implies b1 = - b1 ) ) ;
end;
:: deftheorem Def1 defines |. EXTREAL1:def_1_:_
for x being R_eal holds
( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );
theorem :: EXTREAL1:3
for x being R_eal st 0 <= x holds
|.x.| = x by Def1;
theorem :: EXTREAL1:4
for x being R_eal st x < 0 holds
|.x.| = - x by Def1;
registration
let x be R_eal;
cluster|.x.| -> non negative ;
coherence
not |.x.| is negative
proof
percases ( 0 <= x or x < 0 ) ;
supposeA1: 0 <= x ; ::_thesis: not |.x.| is negative
then |.x.| = x by Def1;
hence not |.x.| is negative by A1; ::_thesis: verum
end;
supposeA2: x < 0 ; ::_thesis: not |.x.| is negative
then |.x.| = - x by Def1;
hence not |.x.| is negative by A2; ::_thesis: verum
end;
end;
end;
end;
theorem :: EXTREAL1:5
for a, b being Real holds a * b = (R_EAL a) * (R_EAL b)
proof
let a, b be Real; ::_thesis: a * b = (R_EAL a) * (R_EAL b)
( R_EAL a = a & R_EAL b = b ) by MEASURE6:def_1;
hence a * b = (R_EAL a) * (R_EAL b) by Th1; ::_thesis: verum
end;
theorem :: EXTREAL1:6
for a, b being Real holds a / b = (R_EAL a) / (R_EAL b)
proof
let a, b be Real; ::_thesis: a / b = (R_EAL a) / (R_EAL b)
( R_EAL a = a & R_EAL b = b ) by MEASURE6:def_1;
hence a / b = (R_EAL a) / (R_EAL b) by Th2; ::_thesis: verum
end;
begin
definition
let F be FinSequence of ExtREAL ;
func Sum F -> R_eal means :Def2: :: EXTREAL1:def 2
ex f being Function of NAT,ExtREAL st
( it = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) );
existence
ex b1 being R_eal ex f being Function of NAT,ExtREAL st
( b1 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) )
proof
defpred S1[ FinSequence of ExtREAL ] means ex f being Function of NAT,ExtREAL st
( f . 0 = 0. & ( for i being Element of NAT st i < len $1 holds
f . (i + 1) = (f . i) + ($1 . (i + 1)) ) );
A1: for F being FinSequence of ExtREAL
for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume S1[F] ; ::_thesis: S1[F ^ <*x*>]
then consider f being Function of NAT,ExtREAL such that
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ;
defpred S2[ Element of NAT , set ] means ( ( $1 <= len F implies $2 = f . $1 ) & ( $1 = (len F) + 1 implies $2 = (f . (len F)) + x ) );
A4: for i being Element of NAT ex g being Element of ExtREAL st S2[i,g]
proof
let i be Element of NAT ; ::_thesis: ex g being Element of ExtREAL st S2[i,g]
percases ( i <> (len F) + 1 or i = (len F) + 1 ) ;
supposeA5: i <> (len F) + 1 ; ::_thesis: ex g being Element of ExtREAL st S2[i,g]
take f . i ; ::_thesis: S2[i,f . i]
thus S2[i,f . i] by A5; ::_thesis: verum
end;
supposeA6: i = (len F) + 1 ; ::_thesis: ex g being Element of ExtREAL st S2[i,g]
take (f . (len F)) + x ; ::_thesis: S2[i,(f . (len F)) + x]
thus S2[i,(f . (len F)) + x] by A6, NAT_1:13; ::_thesis: verum
end;
end;
end;
consider f9 being Function of NAT,ExtREAL such that
A7: for i being Element of NAT holds S2[i,f9 . i] from FUNCT_2:sch_3(A4);
thus S1[F ^ <*x*>] ::_thesis: verum
proof
take f9 ; ::_thesis: ( f9 . 0 = 0. & ( for i being Element of NAT st i < len (F ^ <*x*>) holds
f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) ) )
thus f9 . 0 = 0. by A2, A7; ::_thesis: for i being Element of NAT st i < len (F ^ <*x*>) holds
f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))
thus for i being Element of NAT st i < len (F ^ <*x*>) holds
f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) ::_thesis: verum
proof
let i be Element of NAT ; ::_thesis: ( i < len (F ^ <*x*>) implies f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) )
assume i < len (F ^ <*x*>) ; ::_thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))
then i < (len F) + (len <*x*>) by FINSEQ_1:22;
then i < (len F) + 1 by FINSEQ_1:39;
then A8: i <= len F by NAT_1:13;
then A9: f9 . i = f . i by A7;
percases ( i < len F or i = len F ) by A8, XXREAL_0:1;
supposeA10: i < len F ; ::_thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))
then A11: i + 1 <= len F by INT_1:7;
1 <= i + 1 by NAT_1:12;
then i + 1 in Seg (len F) by A11, FINSEQ_1:1;
then A12: i + 1 in dom F by FINSEQ_1:def_3;
f9 . (i + 1) = f . (i + 1) by A7, A11;
then f9 . (i + 1) = (f9 . i) + (F . (i + 1)) by A3, A9, A10;
hence f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) by A12, FINSEQ_1:def_7; ::_thesis: verum
end;
supposeA13: i = len F ; ::_thesis: f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1))
then f9 . (i + 1) = (f9 . i) + x by A7, A9;
hence f9 . (i + 1) = (f9 . i) + ((F ^ <*x*>) . (i + 1)) by A13, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
end;
end;
A14: S1[ <*> ExtREAL]
proof
reconsider f = NAT --> 0. as Function of NAT,ExtREAL ;
take f ; ::_thesis: ( f . 0 = 0. & ( for i being Element of NAT st i < len (<*> ExtREAL) holds
f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1)) ) )
thus f . 0 = 0. by FUNCOP_1:7; ::_thesis: for i being Element of NAT st i < len (<*> ExtREAL) holds
f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1))
thus for i being Element of NAT st i < len (<*> ExtREAL) holds
f . (i + 1) = (f . i) + ((<*> ExtREAL) . (i + 1)) ; ::_thesis: verum
end;
for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A14, A1);
then consider f being Function of NAT,ExtREAL such that
A15: f . 0 = 0. and
A16: for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ;
take f . (len F) ; ::_thesis: ex f being Function of NAT,ExtREAL st
( f . (len F) = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) )
thus ex f being Function of NAT,ExtREAL st
( f . (len F) = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by A15, A16; ::_thesis: verum
end;
uniqueness
for b1, b2 being R_eal st ex f being Function of NAT,ExtREAL st
( b1 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being Function of NAT,ExtREAL st
( b2 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds
b1 = b2
proof
let g1, g2 be Element of ExtREAL ; ::_thesis: ( ex f being Function of NAT,ExtREAL st
( g1 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being Function of NAT,ExtREAL st
( g2 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) implies g1 = g2 )
given f1 being Function of NAT,ExtREAL such that A17: g1 = f1 . (len F) and
A18: f1 . 0 = 0. and
A19: for i being Element of NAT st i < len F holds
f1 . (i + 1) = (f1 . i) + (F . (i + 1)) ; ::_thesis: ( for f being Function of NAT,ExtREAL holds
( not g2 = f . (len F) or not f . 0 = 0. or ex i being Element of NAT st
( i < len F & not f . (i + 1) = (f . i) + (F . (i + 1)) ) ) or g1 = g2 )
given f2 being Function of NAT,ExtREAL such that A20: g2 = f2 . (len F) and
A21: f2 . 0 = 0. and
A22: for i being Element of NAT st i < len F holds
f2 . (i + 1) = (f2 . i) + (F . (i + 1)) ; ::_thesis: g1 = g2
defpred S1[ Element of NAT ] means ( $1 <= len F implies f1 . $1 = f2 . $1 );
A23: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A24: S1[i] ; ::_thesis: S1[i + 1]
thus S1[i + 1] ::_thesis: verum
proof
assume i + 1 <= len F ; ::_thesis: f1 . (i + 1) = f2 . (i + 1)
then A25: i < len F by NAT_1:13;
then f1 . (i + 1) = (f1 . i) + (F . (i + 1)) by A19;
hence f1 . (i + 1) = f2 . (i + 1) by A22, A24, A25; ::_thesis: verum
end;
end;
A26: S1[ 0 ] by A18, A21;
for i being Element of NAT holds S1[i] from NAT_1:sch_1(A26, A23);
hence g1 = g2 by A17, A20; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Sum EXTREAL1:def_2_:_
for F being FinSequence of ExtREAL
for b2 being R_eal holds
( b2 = Sum F iff ex f being Function of NAT,ExtREAL st
( b2 = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );
theorem Th7: :: EXTREAL1:7
Sum (<*> ExtREAL) = 0.
proof
reconsider F = <*> ExtREAL as FinSequence of ExtREAL ;
ex f being Function of NAT,ExtREAL st
( Sum F = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by Def2;
hence Sum (<*> ExtREAL) = 0. ; ::_thesis: verum
end;
theorem Th8: :: EXTREAL1:8
for a being R_eal holds Sum <*a*> = a
proof
let a be R_eal; ::_thesis: Sum <*a*> = a
set F = <*a*>;
consider f being Function of NAT,ExtREAL such that
A1: Sum <*a*> = f . (len <*a*>) and
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len <*a*> holds
f . (i + 1) = (f . i) + (<*a*> . (i + 1)) by Def2;
A4: f . (0 + 1) = (f . 0) + (<*a*> . (0 + 1)) by A3;
Sum <*a*> = f . 1 by A1, FINSEQ_1:39;
then Sum <*a*> = <*a*> . 1 by A2, A4, XXREAL_3:4
.= a by FINSEQ_1:40 ;
hence Sum <*a*> = a ; ::_thesis: verum
end;
Lm1: for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
let x be Element of ExtREAL ; ::_thesis: Sum (F ^ <*x*>) = (Sum F) + x
consider f being Function of NAT,ExtREAL such that
A1: Sum (F ^ <*x*>) = f . (len (F ^ <*x*>)) and
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len (F ^ <*x*>) holds
f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by Def2;
A4: len (F ^ <*x*>) = (len F) + (len <*x*>) by FINSEQ_1:22
.= (len F) + 1 by FINSEQ_1:39 ;
for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1))
proof
let i be Element of NAT ; ::_thesis: ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) )
A5: 1 <= i + 1 by NAT_1:11;
assume A6: i < len F ; ::_thesis: f . (i + 1) = (f . i) + (F . (i + 1))
then i + 1 <= len F by INT_1:7;
then i + 1 in Seg (len F) by A5, FINSEQ_1:1;
then A7: i + 1 in dom F by FINSEQ_1:def_3;
i < len (F ^ <*x*>) by A4, A6, NAT_1:13;
then f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by A3;
hence f . (i + 1) = (f . i) + (F . (i + 1)) by A7, FINSEQ_1:def_7; ::_thesis: verum
end;
then A8: Sum F = f . (len F) by A2, Def2;
len F < len (F ^ <*x*>) by A4, NAT_1:13;
then f . ((len F) + 1) = (f . (len F)) + ((F ^ <*x*>) . ((len F) + 1)) by A3;
hence Sum (F ^ <*x*>) = (Sum F) + x by A1, A4, A8, FINSEQ_1:42; ::_thesis: verum
end;
theorem :: EXTREAL1:9
for a, b being R_eal holds Sum <*a,b*> = a + b
proof
let a, b be R_eal; ::_thesis: Sum <*a,b*> = a + b
thus Sum <*a,b*> = Sum (<*a*> ^ <*b*>) by FINSEQ_1:def_9
.= (Sum <*a*>) + b by Lm1
.= a + b by Th8 ; ::_thesis: verum
end;
Lm2: for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty
proof
defpred S1[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies Sum $1 <> -infty );
A1: for F being FinSequence of ExtREAL
for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>]
A3: Sum (F ^ <*x*>) = (Sum F) + x by Lm1;
assume not -infty in rng (F ^ <*x*>) ; ::_thesis: Sum (F ^ <*x*>) <> -infty
then A4: not -infty in (rng F) \/ (rng <*x*>) by FINSEQ_1:31;
then not -infty in rng <*x*> by XBOOLE_0:def_3;
then not -infty in {x} by FINSEQ_1:38;
then x <> -infty by TARSKI:def_1;
hence Sum (F ^ <*x*>) <> -infty by A2, A4, A3, XBOOLE_0:def_3, XXREAL_3:17; ::_thesis: verum
end;
A5: S1[ <*> ExtREAL] by Th7;
thus for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A5, A1); ::_thesis: verum
end;
theorem Th10: :: EXTREAL1:10
for F, G being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G holds
Sum (F ^ G) = (Sum F) + (Sum G)
proof
let F, G be FinSequence of ExtREAL ; ::_thesis: ( not -infty in rng F & not -infty in rng G implies Sum (F ^ G) = (Sum F) + (Sum G) )
defpred S1[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies Sum (F ^ $1) = (Sum F) + (Sum $1) );
assume A1: not -infty in rng F ; ::_thesis: ( -infty in rng G or Sum (F ^ G) = (Sum F) + (Sum G) )
A2: for H being FinSequence of ExtREAL
for x being Element of ExtREAL st S1[H] holds
S1[H ^ <*x*>]
proof
let H be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[H] holds
S1[H ^ <*x*>]
let x be Element of ExtREAL ; ::_thesis: ( S1[H] implies S1[H ^ <*x*>] )
assume A3: S1[H] ; ::_thesis: S1[H ^ <*x*>]
thus S1[H ^ <*x*>] ::_thesis: verum
proof
assume not -infty in rng (H ^ <*x*>) ; ::_thesis: Sum (F ^ (H ^ <*x*>)) = (Sum F) + (Sum (H ^ <*x*>))
then A4: not -infty in (rng H) \/ (rng <*x*>) by FINSEQ_1:31;
then not -infty in rng H by XBOOLE_0:def_3;
then A5: Sum H <> -infty by Lm2;
not -infty in rng <*x*> by A4, XBOOLE_0:def_3;
then not -infty in {x} by FINSEQ_1:38;
then A6: x <> -infty by TARSKI:def_1;
A7: Sum F <> -infty by A1, Lm2;
F ^ (H ^ <*x*>) = (F ^ H) ^ <*x*> by FINSEQ_1:32;
hence Sum (F ^ (H ^ <*x*>)) = ((Sum F) + (Sum H)) + x by A3, A4, Lm1, XBOOLE_0:def_3
.= (Sum F) + ((Sum H) + x) by A6, A7, A5, XXREAL_3:29
.= (Sum F) + (Sum (H ^ <*x*>)) by Lm1 ;
::_thesis: verum
end;
end;
assume A8: not -infty in rng G ; ::_thesis: Sum (F ^ G) = (Sum F) + (Sum G)
A9: S1[ <*> ExtREAL]
proof
set H = <*> ExtREAL;
assume not -infty in rng (<*> ExtREAL) ; ::_thesis: Sum (F ^ (<*> ExtREAL)) = (Sum F) + (Sum (<*> ExtREAL))
thus Sum (F ^ (<*> ExtREAL)) = Sum F by FINSEQ_1:34
.= (Sum F) + (Sum (<*> ExtREAL)) by Th7, XXREAL_3:4 ; ::_thesis: verum
end;
for H being FinSequence of ExtREAL holds S1[H] from FINSEQ_2:sch_2(A9, A2);
hence Sum (F ^ G) = (Sum F) + (Sum G) by A8; ::_thesis: verum
end;
Lm3: for n, q being Nat st q in Seg (n + 1) holds
ex p being Permutation of (Seg (n + 1)) st
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 ) )
proof
let n, q be Nat; ::_thesis: ( q in Seg (n + 1) implies ex p being Permutation of (Seg (n + 1)) st
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 ) ) )
defpred S1[ Element of NAT , set ] means ( ( $1 < q implies $2 = $1 ) & ( $1 = q implies $2 = n + 1 ) & ( $1 > q implies $2 = $1 - 1 ) );
assume A1: q in Seg (n + 1) ; ::_thesis: ex p being Permutation of (Seg (n + 1)) st
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 ) )
A2: for i being Element of NAT st i in Seg (n + 1) holds
ex p being Element of NAT st S1[i,p]
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies ex p being Element of NAT st S1[i,p] )
assume i in Seg (n + 1) ; ::_thesis: ex p being Element of NAT st S1[i,p]
percases ( i < q or i = q or i > q ) by XXREAL_0:1;
supposeA3: i < q ; ::_thesis: ex p being Element of NAT st S1[i,p]
take i ; ::_thesis: S1[i,i]
thus S1[i,i] by A3; ::_thesis: verum
end;
supposeA4: i = q ; ::_thesis: ex p being Element of NAT st S1[i,p]
take n + 1 ; ::_thesis: S1[i,n + 1]
thus S1[i,n + 1] by A4; ::_thesis: verum
end;
supposeA5: i > q ; ::_thesis: ex p being Element of NAT st S1[i,p]
1 <= q by A1, FINSEQ_1:1;
then reconsider p = i - 1 as Element of NAT by A5, INT_1:5, XXREAL_0:2;
take p ; ::_thesis: S1[i,p]
thus S1[i,p] by A5; ::_thesis: verum
end;
end;
end;
consider p being FinSequence of NAT such that
A6: dom p = Seg (n + 1) and
A7: for i being Element of NAT st i in Seg (n + 1) holds
S1[i,p /. i] from RECDEF_1:sch_17(A2);
A8: for i being Element of NAT st i in Seg (n + 1) holds
( i = q iff p /. i = n + 1 )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies ( i = q iff p /. i = n + 1 ) )
assume A9: i in Seg (n + 1) ; ::_thesis: ( i = q iff p /. i = n + 1 )
hence ( i = q implies p /. i = n + 1 ) by A7; ::_thesis: ( p /. i = n + 1 implies i = q )
thus ( p /. i = n + 1 implies i = q ) ::_thesis: verum
proof
assume A10: p /. i = n + 1 ; ::_thesis: i = q
percases ( i = q or i < q or i > q ) by XXREAL_0:1;
suppose i = q ; ::_thesis: i = q
hence i = q ; ::_thesis: verum
end;
suppose i < q ; ::_thesis: i = q
then n + 1 < q by A7, A9, A10;
hence i = q by A1, FINSEQ_1:1; ::_thesis: verum
end;
suppose i > q ; ::_thesis: i = q
then i - 1 = n + 1 by A7, A9, A10;
then i >= (n + 1) + 1 ;
then i > n + 1 by NAT_1:13;
hence i = q by A9, FINSEQ_1:1; ::_thesis: verum
end;
end;
end;
end;
A11: 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 ) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) )
assume A12: i in Seg (n + 1) ; ::_thesis: ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
then p /. i = p . i by A6, PARTFUN1:def_6;
hence ( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) by A7, A12; ::_thesis: verum
end;
for i being set holds
( i in rng p iff i in Seg (n + 1) )
proof
let i be set ; ::_thesis: ( i in rng p iff i in Seg (n + 1) )
thus ( i in rng p implies i in Seg (n + 1) ) ::_thesis: ( i in Seg (n + 1) implies i in rng p )
proof
assume i in rng p ; ::_thesis: i in Seg (n + 1)
then consider j being set such that
A13: j in Seg (n + 1) and
A14: p . j = i by A6, FUNCT_1:def_3;
reconsider j = j as Element of NAT by A13;
percases ( j < q or j = q or j > q ) by XXREAL_0:1;
suppose j < q ; ::_thesis: i in Seg (n + 1)
hence i in Seg (n + 1) by A11, A13, A14; ::_thesis: verum
end;
suppose j = q ; ::_thesis: i in Seg (n + 1)
then i = n + 1 by A11, A13, A14;
hence i in Seg (n + 1) by FINSEQ_1:4; ::_thesis: verum
end;
supposeA15: j > q ; ::_thesis: i in Seg (n + 1)
then A16: i = j - 1 by A11, A13, A14;
A17: 1 <= q by A1, FINSEQ_1:1;
then reconsider i = i as Element of NAT by A15, A16, INT_1:5, XXREAL_0:2;
j <= n + 1 by A13, FINSEQ_1:1;
then i <= n by A16, XREAL_1:20;
then A18: i <= n + 1 by NAT_1:12;
1 < i + 1 by A15, A16, A17, XXREAL_0:2;
then 1 <= i by NAT_1:13;
hence i in Seg (n + 1) by A18, FINSEQ_1:1; ::_thesis: verum
end;
end;
end;
thus ( i in Seg (n + 1) implies i in rng p ) ::_thesis: verum
proof
assume A19: i in Seg (n + 1) ; ::_thesis: i in rng p
then reconsider i = i as Element of NAT ;
i <= n + 1 by A19, FINSEQ_1:1;
then A20: ( i = n + 1 or i < n + 1 ) by XXREAL_0:1;
percases ( i < q or ( q <= i & i <= n ) or i = n + 1 ) by A20, NAT_1:13;
suppose i < q ; ::_thesis: i in rng p
then p . i = i by A11, A19;
hence i in rng p by A6, A19, FUNCT_1:3; ::_thesis: verum
end;
supposeA21: ( q <= i & i <= n ) ; ::_thesis: i in rng p
A22: 1 <= i + 1 by NAT_1:12;
i + 1 <= n + 1 by A21, XREAL_1:6;
then A23: i + 1 in Seg (n + 1) by A22, FINSEQ_1:1;
q < i + 1 by A21, NAT_1:13;
then p . (i + 1) = (i + 1) - 1 by A11, A23
.= i ;
hence i in rng p by A6, A23, FUNCT_1:3; ::_thesis: verum
end;
suppose i = n + 1 ; ::_thesis: i in rng p
then p . q = i by A1, A11;
hence i in rng p by A1, A6, FUNCT_1:3; ::_thesis: verum
end;
end;
end;
end;
then A24: rng p = Seg (n + 1) by TARSKI:1;
then A25: p is Function of (Seg (n + 1)),(Seg (n + 1)) by A6, FUNCT_2:1;
A26: for i being Element of NAT st i in Seg (n + 1) & p /. i <> n + 1 holds
( i < q iff p /. i < q )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) & p /. i <> n + 1 implies ( i < q iff p /. i < q ) )
assume that
A27: i in Seg (n + 1) and
A28: p /. i <> n + 1 ; ::_thesis: ( i < q iff p /. i < q )
thus ( i < q implies p /. i < q ) by A7, A27; ::_thesis: ( p /. i < q implies i < q )
thus ( p /. i < q implies i < q ) ::_thesis: verum
proof
assume A29: p /. i < q ; ::_thesis: i < q
percases ( i < q or i = q or i > q ) by XXREAL_0:1;
suppose i < q ; ::_thesis: i < q
hence i < q ; ::_thesis: verum
end;
suppose i = q ; ::_thesis: i < q
hence i < q by A7, A27, A28; ::_thesis: verum
end;
supposeA30: i > q ; ::_thesis: i < q
then p /. i = i - 1 by A7, A27;
then (i - 1) + 1 < q + 1 by A29, XREAL_1:8;
hence i < q by A30, NAT_1:13; ::_thesis: verum
end;
end;
end;
end;
for i1, i2 being set st i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 holds
i1 = i2
proof
let i1, i2 be set ; ::_thesis: ( i1 in Seg (n + 1) & i2 in Seg (n + 1) & p . i1 = p . i2 implies i1 = i2 )
assume that
A31: i1 in Seg (n + 1) and
A32: i2 in Seg (n + 1) and
A33: p . i1 = p . i2 ; ::_thesis: i1 = i2
reconsider i1 = i1 as Element of NAT by A31;
A34: p /. i1 = p . i1 by A6, A31, PARTFUN1:def_6;
reconsider i2 = i2 as Element of NAT by A32;
A35: p /. i2 = p . i2 by A6, A32, PARTFUN1:def_6;
percases ( p /. i1 = n + 1 or ( p /. i1 <> n + 1 & p /. i1 < q ) or ( p /. i1 <> n + 1 & p /. i1 >= q ) ) ;
supposeA36: p /. i1 = n + 1 ; ::_thesis: i1 = i2
then i1 = q by A8, A31;
hence i1 = i2 by A8, A32, A33, A34, A35, A36; ::_thesis: verum
end;
supposeA37: ( p /. i1 <> n + 1 & p /. i1 < q ) ; ::_thesis: i1 = i2
then i1 < q by A26, A31;
then A38: p /. i1 = i1 by A7, A31;
i2 < q by A26, A32, A33, A34, A35, A37;
hence i1 = i2 by A7, A32, A33, A34, A35, A38; ::_thesis: verum
end;
supposeA39: ( p /. i1 <> n + 1 & p /. i1 >= q ) ; ::_thesis: i1 = i2
then A40: i1 <> q by A8, A31;
i1 >= q by A26, A31, A39;
then i1 > q by A40, XXREAL_0:1;
then A41: p /. i1 = i1 - 1 by A7, A31;
A42: i2 <> q by A8, A32, A33, A34, A35, A39;
i2 >= q by A26, A32, A33, A34, A35, A39;
then i2 > q by A42, XXREAL_0:1;
then p /. i2 = i2 - 1 by A7, A32;
hence i1 = i2 by A6, A32, A33, A34, A41, PARTFUN1:def_6, XCMPLX_1:19; ::_thesis: verum
end;
end;
end;
then p is one-to-one by A6, FUNCT_1:def_4;
then reconsider p = p as Permutation of (Seg (n + 1)) by A24, A25, FUNCT_2:57;
take p ; ::_thesis: 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 ) )
thus 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; ::_thesis: verum
end;
Lm4: for n, q being Nat
for s, p being Permutation of (Seg (n + 1))
for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( 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
p * (s9 | n) is Permutation of (Seg n)
proof
let n, q be Nat; ::_thesis: for s, p being Permutation of (Seg (n + 1))
for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( 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
p * (s9 | n) is Permutation of (Seg n)
let s, p be Permutation of (Seg (n + 1)); ::_thesis: for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( 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
p * (s9 | n) is Permutation of (Seg n)
let s9 be FinSequence of Seg (n + 1); ::_thesis: ( s9 = s & q = s . (n + 1) & ( 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 p * (s9 | n) is Permutation of (Seg n) )
assume that
A1: s9 = s and
A2: q = s . (n + 1) and
A3: 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: p * (s9 | n) is Permutation of (Seg n)
A4: dom p = Seg (n + 1) by FUNCT_2:def_1;
reconsider r = p * (s9 | n) as FinSequence of Seg (n + 1) by FINSEQ_2:32;
A5: 0 + n <= 1 + n by XREAL_1:6;
then A6: Seg n c= Seg (n + 1) by FINSEQ_1:5;
s9 | n = s9 | (Seg n) by FINSEQ_1:def_15;
then A7: s9 | n is one-to-one by A1, FUNCT_1:52;
A8: rng p = Seg (n + 1) by FUNCT_2:def_3;
A9: dom s = Seg (n + 1) by FUNCT_2:def_1;
then len s9 = n + 1 by A1, FINSEQ_1:def_3;
then len (s9 | n) = n by A5, FINSEQ_1:59;
then len r = n by FINSEQ_2:33;
then A10: dom r = Seg n by FINSEQ_1:def_3;
A11: rng s = Seg (n + 1) by FUNCT_2:def_3;
then q in Seg (n + 1) by A2, A9, FINSEQ_1:4, FUNCT_1:3;
then A12: q <= n + 1 by FINSEQ_1:1;
for i being set holds
( i in rng r iff i in Seg n )
proof
let i be set ; ::_thesis: ( i in rng r iff i in Seg n )
thus ( i in rng r implies i in Seg n ) ::_thesis: ( i in Seg n implies i in rng r )
proof
assume i in rng r ; ::_thesis: i in Seg n
then consider j being set such that
A13: j in Seg n and
A14: r . j = i by A10, FUNCT_1:def_3;
reconsider j = j as Element of NAT by A13;
A15: j <= n by A13, FINSEQ_1:1;
then A16: (s9 | n) . j = s . j by A1, FINSEQ_3:112;
then A17: i = p . (s . j) by A10, A13, A14, FUNCT_1:12;
s . j in dom p by A9, A11, A4, A6, A13, FUNCT_1:3;
then A18: p . (s . j) in rng p by FUNCT_1:3;
then reconsider i = i as Element of NAT by A8, A10, A13, A14, A16, FUNCT_1:12;
A19: n + 1 in dom s by A9, FINSEQ_1:4;
A20: s . j in Seg (n + 1) by A9, A11, A6, A13, FUNCT_1:3;
then reconsider q1 = s . j as Element of NAT ;
j < n + 1 by A15, NAT_1:13;
then A21: q1 <> q by A2, A9, A6, A13, A19, FUNCT_1:def_4;
percases ( q1 < q or q1 > q ) by A21, XXREAL_0:1;
suppose q1 < q ; ::_thesis: i in Seg n
then i < q by A3, A17, A20;
then i < n + 1 by A12, XXREAL_0:2;
then A22: i <= n by NAT_1:13;
1 <= i by A8, A17, A18, FINSEQ_1:1;
hence i in Seg n by A22, FINSEQ_1:1; ::_thesis: verum
end;
supposeA23: q1 > q ; ::_thesis: i in Seg n
A24: q1 <= n + 1 by A20, FINSEQ_1:1;
i = q1 - 1 by A3, A17, A20, A23;
then A25: i <= n by A24, XREAL_1:20;
1 <= i by A8, A17, A18, FINSEQ_1:1;
hence i in Seg n by A25, FINSEQ_1:1; ::_thesis: verum
end;
end;
end;
assume A26: i in Seg n ; ::_thesis: i in rng r
then reconsider i = i as Element of NAT ;
percases ( i < q or i >= q ) ;
supposeA27: i < q ; ::_thesis: i in rng r
then A28: p . i = i by A3, A6, A26;
consider j being set such that
A29: j in dom s and
A30: i = s . j by A11, A6, A26, FUNCT_1:def_3;
j in Seg (n + 1) by A29;
then reconsider j = j as Element of NAT ;
j <= n + 1 by A29, FINSEQ_1:1;
then j < n + 1 by A2, A27, A30, XXREAL_0:1;
then A31: j <= n by NAT_1:13;
1 <= j by A29, FINSEQ_1:1;
then A32: j in dom r by A10, A31, FINSEQ_1:1;
(s9 | n) . j = s . j by A1, A31, FINSEQ_3:112;
then r . j = i by A28, A30, A32, FUNCT_1:12;
hence i in rng r by A32, FUNCT_1:3; ::_thesis: verum
end;
supposeA33: i >= q ; ::_thesis: i in rng r
i <= n by A26, FINSEQ_1:1;
then A34: i + 1 <= n + 1 by XREAL_1:6;
1 <= i + 1 by NAT_1:12;
then A35: i + 1 in Seg (n + 1) by A34, FINSEQ_1:1;
then consider j being set such that
A36: j in dom s and
A37: i + 1 = s . j by A11, FUNCT_1:def_3;
j in Seg (n + 1) by A36;
then reconsider j = j as Element of NAT ;
A38: j <= n + 1 by A36, FINSEQ_1:1;
j <> n + 1 by A2, A33, A37, NAT_1:13;
then j < n + 1 by A38, XXREAL_0:1;
then A39: j <= n by NAT_1:13;
1 <= j by A36, FINSEQ_1:1;
then A40: j in Seg n by A39, FINSEQ_1:1;
i + 1 > q by A33, NAT_1:13;
then A41: p . (i + 1) = (i + 1) - 1 by A3, A35
.= i ;
(s9 | n) . j = s . j by A1, A39, FINSEQ_3:112;
then r . j = p . (s . j) by A10, A40, FUNCT_1:12;
hence i in rng r by A10, A37, A41, A40, FUNCT_1:3; ::_thesis: verum
end;
end;
end;
then A42: rng r = Seg n by TARSKI:1;
then p * (s9 | n) is Function of (Seg n),(Seg n) by A10, FUNCT_2:1;
hence p * (s9 | n) is Permutation of (Seg n) by A42, A7, FUNCT_2:57; ::_thesis: verum
end;
Lm5: for n, q being Nat
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
proof
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 by A2, FINSEQ_1:1;
then q - 1 >= 1 - 1 by XREAL_1:9;
then A7: q -' 1 = q - 1 by XREAL_0:def_2;
set H1 = H | n;
A8: H | n = ((H | n) | (q -' 1)) ^ ((H | n) /^ (q -' 1)) by RFINSEQ:8;
reconsider p9 = p as FinSequence of Seg (n + 1) by FINSEQ_2:25;
dom p = Seg (n + 1) by FUNCT_2:def_1;
then A9: len p9 = n + 1 by FINSEQ_1:def_3;
A10: q <= n + 1 by A2, FINSEQ_1:1;
then A11: q -' 1 <= (n + 1) - 1 by A7, XREAL_1:9;
A12: dom H = Seg (n + 1) by A3, FINSEQ_1:def_3;
then H is Function of (Seg (n + 1)),ExtREAL by FINSEQ_2:26;
then A13: len F = n + 1 by A1, A9, FINSEQ_2:33;
then A14: len (F /^ q) = (n + 1) - q by A10, RFINSEQ:def_1;
A15: n <= n + 1 by NAT_1:11;
then A16: len (F | (q -' 1)) = q -' 1 by A11, A13, FINSEQ_1:59, XXREAL_0:2;
A17: dom F = Seg (n + 1) by A13, FINSEQ_1:def_3;
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 that
A19: 1 <= i and
A20: i <= q -' 1 ; ::_thesis: (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i
A21: (F | (q -' 1)) . i = F . i by A20, FINSEQ_3:112;
A22: (H | n) . i = H . i by A11, A20, FINSEQ_3:112, XXREAL_0:2;
A23: ((H | n) | (q -' 1)) . i = (H | n) . i by A20, FINSEQ_3:112;
A24: i < (q -' 1) + 1 by A20, NAT_1:13;
i <= n by A11, A20, XXREAL_0:2;
then i <= n + 1 by A15, XXREAL_0:2;
then A25: i in Seg (n + 1) by A19, FINSEQ_1:1;
then F . i = H . (p . i) by A1, A17, FUNCT_1:12;
hence (F | (q -' 1)) . i = ((H | n) | (q -' 1)) . i by A5, A7, A21, A23, A22, A25, A24; ::_thesis: verum
end;
0 + n <= 1 + n by XREAL_1:6;
then A26: len (H | n) = n by A3, FINSEQ_1:59;
then A27: len ((H | n) | (q -' 1)) = q -' 1 by A11, FINSEQ_1:59;
A28: len ((H | n) /^ (q -' 1)) = n - (q - 1) by A7, A11, A26, RFINSEQ:def_1;
for i being Nat st 1 <= i & i <= (n + 1) - q holds
(F /^ q) . i = ((H | n) /^ (q -' 1)) . i
proof
reconsider n1 = (n + 1) - q as Element of NAT by A10, INT_1:5;
let i be Nat; ::_thesis: ( 1 <= i & i <= (n + 1) - q implies (F /^ q) . i = ((H | n) /^ (q -' 1)) . i )
assume that
A29: 1 <= i and
A30: i <= (n + 1) - q ; ::_thesis: (F /^ q) . i = ((H | n) /^ (q -' 1)) . i
A31: i + q <= n + 1 by A30, XREAL_1:19;
A32: i in Seg n1 by A29, A30, FINSEQ_1:1;
then i in dom ((H | n) /^ (q -' 1)) by A28, FINSEQ_1:def_3;
then A33: ((H | n) /^ (q -' 1)) . i = (H | n) . (i + (q -' 1)) by A11, A26, RFINSEQ:def_1;
i + (q -' 1) = (i + q) - 1 by A7;
then i + (q -' 1) <= n by A31, XREAL_1:20;
then A34: ((H | n) /^ (q -' 1)) . i = H . ((i + q) - 1) by A7, A33, FINSEQ_3:112;
A35: 1 <= i + q by A29, NAT_1:12;
then i + q in dom F by A17, A31, FINSEQ_1:1;
then A36: F . (i + q) = H . (p . (i + q)) by A1, FUNCT_1:12;
dom (F /^ q) = Seg n1 by A14, FINSEQ_1:def_3;
then A37: (F /^ q) . i = F . (i + q) by A10, A13, A32, RFINSEQ:def_1;
i + q >= 1 + q by A29, XREAL_1:6;
then A38: i + q > q by NAT_1:13;
i + q in Seg (n + 1) by A31, A35, FINSEQ_1:1;
hence (F /^ q) . i = ((H | n) /^ (q -' 1)) . i by A5, A37, A34, A36, A38; ::_thesis: verum
end;
then A39: F /^ q = (H | n) /^ (q -' 1) by A14, A28, FINSEQ_1:14;
A40: F = ((F | (q -' 1)) ^ <*(F . q)*>) ^ (F /^ q) by A6, A10, A13, FINSEQ_5:84;
then A41: rng F = (rng ((F | (q -' 1)) ^ <*(F . q)*>)) \/ (rng (F /^ q)) by FINSEQ_1:31;
p . q = n + 1 by A2, A5;
then A42: F . q = H . (n + 1) by A1, A2, A17, FUNCT_1:12;
A43: H | n = H | (Seg n) by FINSEQ_1:def_15;
then rng (H | n) c= rng H by RELAT_1:70;
then not -infty in rng (H | n) by A4;
then A44: not -infty in (rng ((H | n) | (q -' 1))) \/ (rng ((H | n) /^ (q -' 1))) by A8, FINSEQ_1:31;
then A45: not -infty in rng ((H | n) | (q -' 1)) by XBOOLE_0:def_3;
A46: not -infty in rng F by A1, A4, FUNCT_1:14;
then A47: not -infty in rng ((F | (q -' 1)) ^ <*(F . q)*>) by A41, XBOOLE_0:def_3;
then A48: not -infty in (rng (F | (q -' 1))) \/ (rng <*(F . q)*>) by FINSEQ_1:31;
then not -infty in rng (F | (q -' 1)) by XBOOLE_0:def_3;
then A49: Sum (F | (q -' 1)) <> -infty by Lm2;
not -infty in rng <*(F . q)*> by A48, XBOOLE_0:def_3;
then not -infty in {(F . q)} by FINSEQ_1:39;
then A50: -infty <> F . q by TARSKI:def_1;
A51: not -infty in rng (F /^ q) by A46, A41, XBOOLE_0:def_3;
then A52: Sum (F /^ q) <> -infty by Lm2;
A53: H | (n + 1) = H | (Seg (n + 1)) by FINSEQ_1:def_15;
H | (n + 1) = H by A3, FINSEQ_1:58;
then A54: H = (H | n) ^ <*(H . (n + 1))*> by A12, A43, A53, FINSEQ_1:4, FINSEQ_5:10;
A55: not -infty in rng ((H | n) /^ (q -' 1)) by A44, XBOOLE_0:def_3;
thus Sum F = (Sum ((F | (q -' 1)) ^ <*(F . q)*>)) + (Sum (F /^ q)) by A40, A47, A51, Th10
.= ((Sum (F | (q -' 1))) + (F . q)) + (Sum (F /^ q)) by Lm1
.= ((Sum (F | (q -' 1))) + (Sum (F /^ q))) + (F . q) by A50, A49, A52, XXREAL_3:29
.= ((Sum ((H | n) | (q -' 1))) + (Sum ((H | n) /^ (q -' 1)))) + (H . (n + 1)) by A16, A27, A18, A42, A39, FINSEQ_1:14
.= (Sum (H | n)) + (H . (n + 1)) by A8, A45, A55, Th10
.= Sum H by A54, Lm1 ; ::_thesis: verum
end;
theorem :: EXTREAL1:11
for F, G being FinSequence of ExtREAL
for s being Permutation of (dom F) st G = F * s & not -infty in rng F holds
Sum F = Sum G
proof
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 (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;
A4: 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 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 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; ::_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 A9, 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;
len (G | n) = n by A20, A15, FINSEQ_1:59;
hence G | n = (H | n) * p1 by A30, A31, FINSEQ_1:14; ::_thesis: 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; ::_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 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;
A52: for n being non empty 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 ; ::_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
end;