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