extreal1.miz



    begin

    definition

      let x,y be R_eal;

      :: original: *

      redefine

      func x * y -> R_eal ;

      coherence by XXREAL_0:def 1;

    end

    theorem :: EXTREAL1:1

    for x,y be ExtReal holds for a,b be Real holds x = a & y = b implies (x * y) = (a * b) by XXREAL_3:def 5;

    definition

      let x,y be ExtReal;

      :: original: /

      redefine

      func x / y -> R_eal ;

      coherence by XXREAL_0:def 1;

    end

    theorem :: EXTREAL1:2

    for x,y be ExtReal holds for a,b be Real st x = a & y = b holds (x / y) = (a / b);

    definition

      let x be ExtReal;

      :: EXTREAL1:def1

      func |.x.| -> R_eal equals

      : Def1: x if 0 <= x

      otherwise ( - x);

      coherence by XXREAL_0:def 1;

      consistency ;

      projectivity ;

    end

    registration

      let x be Real, a be Complex;

      identify |.a.| with |.x.| when x = a;

      compatibility

      proof

        assume

         A1: x = a;

        per cases ;

          suppose

           A2: 0 <= x;

          

          hence |.x.| = a by A1, Def1

          .= |.a.| by A2, A1, ABSVALUE:def 1;

        end;

          suppose

           A3: 0 > x;

          

          hence |.x.| = ( - x qua ExtReal) by Def1

          .= ( - a) by A1

          .= |.a.| by A3, A1, ABSVALUE:def 1;

        end;

      end;

    end

    theorem :: EXTREAL1:3

    for x be R_eal st 0 <= x holds |.x.| = x by Def1;

    theorem :: EXTREAL1:4

    for x be R_eal st x < 0 holds |.x.| = ( - x) by Def1;

    registration

      let x be R_eal;

      cluster |.x.| -> non negative;

      coherence

      proof

        per cases ;

          suppose

           A1: 0 <= x;

          then |.x.| = x by Def1;

          hence thesis by A1;

        end;

          suppose

           A2: x < 0 ;

          then |.x.| = ( - x) by Def1;

          hence thesis by A2;

        end;

      end;

    end

    ::$Canceled

    begin

    definition

      let F be FinSequence of ExtREAL ;

      :: EXTREAL1:def2

      func Sum (F) -> R_eal means

      : Def2: ex f be sequence of ExtREAL st it = (f . ( len F)) & (f . 0 ) = 0. & for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)));

      existence

      proof

        defpred P[ FinSequence of ExtREAL ] means ex f be sequence of ExtREAL st (f . 0 ) = 0. & for i be Element of NAT st i < ( len $1) holds (f . (i + 1)) = ((f . i) + ($1 . (i + 1)));

        

         A1: for F be FinSequence of ExtREAL holds for x be Element of ExtREAL st P[F] holds P[(F ^ <*x*>)]

        proof

          let F be FinSequence of ExtREAL ;

          let x be Element of ExtREAL ;

          assume P[F];

          then

          consider f be sequence of ExtREAL such that

           A2: (f . 0 ) = 0. and

           A3: for i be Element of NAT st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)));

          defpred R[ 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 be Element of NAT holds ex g be Element of ExtREAL st R[i, g]

          proof

            let i be Element of NAT ;

            per cases ;

              suppose

               A5: i <> (( len F) + 1);

              take (f . i);

              thus thesis by A5;

            end;

              suppose

               A6: i = (( len F) + 1);

              take ((f . ( len F)) + x);

              thus thesis by A6, NAT_1: 13;

            end;

          end;

          consider f9 be sequence of ExtREAL such that

           A7: for i be Element of NAT holds R[i, (f9 . i)] from FUNCT_2:sch 3( A4);

          thus P[(F ^ <*x*>)]

          proof

            take f9;

            thus (f9 . 0 ) = 0. by A2, A7;

            thus for i be Element of NAT st i < ( len (F ^ <*x*>)) holds (f9 . (i + 1)) = ((f9 . i) + ((F ^ <*x*>) . (i + 1)))

            proof

              let i be Element of NAT ;

              assume i < ( len (F ^ <*x*>));

              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;

              per cases by A8, XXREAL_0: 1;

                suppose

                 A10: i < ( len F);

                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 thesis by A12, FINSEQ_1:def 7;

              end;

                suppose

                 A13: i = ( len F);

                then (f9 . (i + 1)) = ((f9 . i) + x) by A7, A9;

                hence thesis by A13, FINSEQ_1: 42;

              end;

            end;

          end;

        end;

        

         A14: P[( <*> ExtREAL )]

        proof

          reconsider f = ( NAT --> 0. ) as sequence of ExtREAL ;

          take f;

          thus (f . 0 ) = 0. by FUNCOP_1: 7;

          thus thesis;

        end;

        for F be FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2( A14, A1);

        then

        consider f be sequence of ExtREAL such that

         A15: (f . 0 ) = 0. and

         A16: for i be Element of NAT st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)));

        

         A17: for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)))

        proof

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          hence thesis by A16;

        end;

        take (f . ( len F));

        thus thesis by A15, A17;

      end;

      uniqueness

      proof

        let g1,g2 be Element of ExtREAL ;

        given f1 be sequence of ExtREAL such that

         A18: g1 = (f1 . ( len F)) and

         A19: (f1 . 0 ) = 0. and

         A20: for i be Nat st i < ( len F) holds (f1 . (i + 1)) = ((f1 . i) + (F . (i + 1)));

        given f2 be sequence of ExtREAL such that

         A21: g2 = (f2 . ( len F)) and

         A22: (f2 . 0 ) = 0. and

         A23: for i be Nat st i < ( len F) holds (f2 . (i + 1)) = ((f2 . i) + (F . (i + 1)));

        defpred P[ Nat] means $1 <= ( len F) implies (f1 . $1) = (f2 . $1);

        

         A24: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat;

          assume

           A25: P[i];

          thus P[(i + 1)]

          proof

            assume (i + 1) <= ( len F);

            then

             A26: i < ( len F) by NAT_1: 13;

            then (f1 . (i + 1)) = ((f1 . i) + (F . (i + 1))) by A20;

            hence thesis by A23, A25, A26;

          end;

        end;

        

         A27: P[ 0 ] by A19, A22;

        for i be Nat holds P[i] from NAT_1:sch 2( A27, A24);

        hence thesis by A18, A21;

      end;

    end

    theorem :: EXTREAL1:7

    

     Th5: ( Sum ( <*> ExtREAL )) = 0.

    proof

      reconsider F = ( <*> ExtREAL ) as FinSequence of ExtREAL ;

      ex f be sequence of ExtREAL st ( Sum F) = (f . ( len F)) & (f . 0 ) = 0. & for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1))) by Def2;

      hence thesis;

    end;

    theorem :: EXTREAL1:8

    

     Th6: for a be R_eal holds ( Sum <*a*>) = a

    proof

      let a be R_eal;

      set F = <*a*>;

      consider f be sequence of ExtREAL such that

       A1: ( Sum F) = (f . ( len F)) and

       A2: (f . 0 ) = 0. and

       A3: for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1))) by Def2;

      

       A4: (f . ( 0 + 1)) = ((f . 0 ) + (F . ( 0 + 1))) by A3;

      ( Sum F) = (f . 1) by A1, FINSEQ_1: 39;

      

      then ( Sum F) = (F . 1) by A2, A4, XXREAL_3: 4

      .= a by FINSEQ_1: 40;

      hence thesis;

    end;

    

     Lm1: for F be FinSequence of ExtREAL , x be Element of ExtREAL holds ( Sum (F ^ <*x*>)) = (( Sum F) + x)

    proof

      let F be FinSequence of ExtREAL , x be Element of ExtREAL ;

      consider f be sequence of ExtREAL such that

       A1: ( Sum (F ^ <*x*>)) = (f . ( len (F ^ <*x*>))) and

       A2: (f . 0 ) = 0. and

       A3: for i be 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 be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)))

      proof

        let i be Nat;

        

         A5: 1 <= (i + 1) by NAT_1: 11;

        assume

         A6: i < ( len F);

        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 thesis by A7, FINSEQ_1:def 7;

      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 thesis by A1, A4, A8, FINSEQ_1: 42;

    end;

    theorem :: EXTREAL1:9

    for a,b be R_eal holds ( Sum <*a, b*>) = (a + b)

    proof

      let a,b be R_eal;

      

      thus ( Sum <*a, b*>) = ( Sum ( <*a*> ^ <*b*>)) by FINSEQ_1:def 9

      .= (( Sum <*a*>) + b) by Lm1

      .= (a + b) by Th6;

    end;

    

     Lm2: for F be FinSequence of ExtREAL st not -infty in ( rng F) holds ( Sum F) <> -infty

    proof

      defpred P[ FinSequence of ExtREAL ] means not -infty in ( rng $1) implies ( Sum $1) <> -infty ;

      

       A1: for F be FinSequence of ExtREAL holds for x be Element of ExtREAL st P[F] holds P[(F ^ <*x*>)]

      proof

        let F be FinSequence of ExtREAL ;

        let x be Element of ExtREAL ;

        assume

         A2: P[F];

        

         A3: ( Sum (F ^ <*x*>)) = (( Sum F) + x) by Lm1;

        assume not -infty in ( rng (F ^ <*x*>));

        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 thesis by A2, A4, A3, XBOOLE_0:def 3, XXREAL_3: 17;

      end;

      

       A5: P[( <*> ExtREAL )] by Th5;

      thus for F be FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2( A5, A1);

    end;

    theorem :: EXTREAL1:10

    

     Th8: for F,G be 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 ;

      defpred P[ FinSequence of ExtREAL ] means not -infty in ( rng $1) implies ( Sum (F ^ $1)) = (( Sum F) + ( Sum $1));

      assume

       A1: not -infty in ( rng F);

      

       A2: for H be FinSequence of ExtREAL holds for x be Element of ExtREAL st P[H] holds P[(H ^ <*x*>)]

      proof

        let H be FinSequence of ExtREAL ;

        let x be Element of ExtREAL ;

        assume

         A3: P[H];

        thus P[(H ^ <*x*>)]

        proof

          assume not -infty in ( rng (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;

        end;

      end;

      assume

       A8: not -infty in ( rng G);

      

       A9: P[( <*> ExtREAL )]

      proof

        set H = ( <*> ExtREAL );

        assume not -infty in ( rng H);

        

        thus ( Sum (F ^ H)) = ( Sum F) by FINSEQ_1: 34

        .= (( Sum F) + ( Sum H)) by Th5, XXREAL_3: 4;

      end;

      for H be FinSequence of ExtREAL holds P[H] from FINSEQ_2:sch 2( A9, A2);

      hence thesis by A8;

    end;

    

     Lm3: for n,q be Nat st q in ( Seg (n + 1)) holds ex p be Permutation of ( Seg (n + 1)) st for i be 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;

      defpred R[ 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));

      

       A2: for i be Nat st i in ( Seg (n + 1)) holds ex p be Element of NAT st R[i, p]

      proof

        let i be Nat;

        assume i in ( Seg (n + 1));

        per cases by XXREAL_0: 1;

          suppose

           A3: i < q;

          take i;

          i in NAT by ORDINAL1:def 12;

          hence thesis by A3;

        end;

          suppose

           A4: i = q;

          take (n + 1);

          thus thesis by A4;

        end;

          suppose

           A5: i > q;

          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;

          thus thesis by A5;

        end;

      end;

      consider p be FinSequence of NAT such that

       A6: ( dom p) = ( Seg (n + 1)) and

       A7: for i be Nat st i in ( Seg (n + 1)) holds R[i, (p /. i)] from RECDEF_1:sch 17( A2);

      

       A8: for i be Element of NAT st i in ( Seg (n + 1)) holds i = q iff (p /. i) = (n + 1)

      proof

        let i be Element of NAT ;

        assume

         A9: i in ( Seg (n + 1));

        hence i = q implies (p /. i) = (n + 1) by A7;

        thus (p /. i) = (n + 1) implies i = q

        proof

          assume

           A10: (p /. i) = (n + 1);

          per cases by XXREAL_0: 1;

            suppose i = q;

            hence thesis;

          end;

            suppose i < q;

            then (n + 1) < q by A7, A9, A10;

            hence thesis by A1, FINSEQ_1: 1;

          end;

            suppose 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 thesis by A9, FINSEQ_1: 1;

          end;

        end;

      end;

      

       A11: for i be 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 ;

        assume

         A12: i in ( Seg (n + 1));

        then (p /. i) = (p . i) by A6, PARTFUN1:def 6;

        hence thesis by A7, A12;

      end;

      for i be object holds i in ( rng p) iff i in ( Seg (n + 1))

      proof

        let i be object;

        thus i in ( rng p) implies i in ( Seg (n + 1))

        proof

          assume i in ( rng p);

          then

          consider j be object such that

           A13: j in ( Seg (n + 1)) and

           A14: (p . j) = i by A6, FUNCT_1:def 3;

          reconsider j as Element of NAT by A13;

          per cases by XXREAL_0: 1;

            suppose j < q;

            hence thesis by A11, A13, A14;

          end;

            suppose j = q;

            then i = (n + 1) by A11, A13, A14;

            hence thesis by FINSEQ_1: 4;

          end;

            suppose

             A15: j > q;

            then

             A16: i = (j - 1) by A11, A13, A14;

            

             A17: 1 <= q by A1, FINSEQ_1: 1;

            then

            reconsider 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 thesis by A18, FINSEQ_1: 1;

          end;

        end;

        thus i in ( Seg (n + 1)) implies i in ( rng p)

        proof

          assume

           A19: i in ( Seg (n + 1));

          then

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

          per cases by A20, NAT_1: 13;

            suppose i < q;

            then (p . i) = i by A11, A19;

            hence thesis by A6, A19, FUNCT_1: 3;

          end;

            suppose

             A21: q <= i & i <= n;

            

             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 thesis by A6, A23, FUNCT_1: 3;

          end;

            suppose i = (n + 1);

            then (p . q) = i by A1, A11;

            hence thesis by A1, A6, FUNCT_1: 3;

          end;

        end;

      end;

      then

       A24: ( rng p) = ( Seg (n + 1)) by TARSKI: 2;

      then

       A25: p is Function of ( Seg (n + 1)), ( Seg (n + 1)) by A6, FUNCT_2: 1;

      

       A26: for i be 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 ;

        assume that

         A27: i in ( Seg (n + 1)) and

         A28: (p /. i) <> (n + 1);

        thus i < q implies (p /. i) < q by A7, A27;

        thus (p /. i) < q implies i < q

        proof

          assume

           A29: (p /. i) < q;

          per cases by XXREAL_0: 1;

            suppose i < q;

            hence thesis;

          end;

            suppose i = q;

            hence thesis by A7, A27, A28;

          end;

            suppose

             A30: i > q;

            then (p /. i) = (i - 1) by A7, A27;

            then ((i - 1) + 1) < (q + 1) by A29, XREAL_1: 8;

            hence thesis by A30, NAT_1: 13;

          end;

        end;

      end;

      for i1,i2 be object st i1 in ( Seg (n + 1)) & i2 in ( Seg (n + 1)) & (p . i1) = (p . i2) holds i1 = i2

      proof

        let i1,i2 be object;

        assume that

         A31: i1 in ( Seg (n + 1)) and

         A32: i2 in ( Seg (n + 1)) and

         A33: (p . i1) = (p . i2);

        reconsider i1 as Element of NAT by A31;

        

         A34: (p /. i1) = (p . i1) by A6, A31, PARTFUN1:def 6;

        reconsider i2 as Element of NAT by A32;

        

         A35: (p /. i2) = (p . i2) by A6, A32, PARTFUN1:def 6;

        per cases ;

          suppose

           A36: (p /. i1) = (n + 1);

          then i1 = q by A8, A31;

          hence thesis by A8, A32, A33, A34, A35, A36;

        end;

          suppose

           A37: (p /. i1) <> (n + 1) & (p /. i1) < q;

          then i1 < q by A26, A31;

          then

           A38: (p /. i1) = i1 by A7, A31;

          i2 < q by A26, A32, A33, A34, A35, A37;

          hence thesis by A7, A32, A33, A34, A35, A38;

        end;

          suppose

           A39: (p /. i1) <> (n + 1) & (p /. i1) >= q;

          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 thesis by A6, A32, A33, A34, A41, PARTFUN1:def 6, XCMPLX_1: 19;

        end;

      end;

      then p is one-to-one by A6, FUNCT_1:def 4;

      then

      reconsider p as Permutation of ( Seg (n + 1)) by A24, A25, FUNCT_2: 57;

      take p;

      thus thesis by A11;

    end;

    

     Lm4: for n,q be Nat, s,p be Permutation of ( Seg (n + 1)), s9 be FinSequence of ( Seg (n + 1)) st s9 = s & q = (s . (n + 1)) & for i be 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, s,p be Permutation of ( Seg (n + 1)), s9 be FinSequence of ( Seg (n + 1));

      assume that

       A1: s9 = s and

       A2: q = (s . (n + 1)) and

       A3: for i be 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));

      

       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 be object holds i in ( rng r) iff i in ( Seg n)

      proof

        let i be object;

        thus i in ( rng r) implies i in ( Seg n)

        proof

          assume i in ( rng r);

          then

          consider j be object such that

           A13: j in ( Seg n) and

           A14: (r . j) = i by A10, FUNCT_1:def 3;

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

          per cases by A21, XXREAL_0: 1;

            suppose q1 < q;

            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 A17, A18, FINSEQ_1: 1;

            hence thesis by A22, FINSEQ_1: 1;

          end;

            suppose

             A23: q1 > q;

            

             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 A17, A18, FINSEQ_1: 1;

            hence thesis by A25, FINSEQ_1: 1;

          end;

        end;

        assume

         A26: i in ( Seg n);

        then

        reconsider i as Element of NAT ;

        per cases ;

          suppose

           A27: i < q;

          then

           A28: (p . i) = i by A3, A6, A26;

          consider j be object 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 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 thesis by A32, FUNCT_1: 3;

        end;

          suppose

           A33: i >= q;

          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 be object 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 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 thesis by A10, A37, A41, A40, FUNCT_1: 3;

        end;

      end;

      then

       A42: ( rng r) = ( Seg n) by TARSKI: 2;

      then (p * (s9 | n)) is Function of ( Seg n), ( Seg n) by A10, FUNCT_2: 1;

      hence thesis by A42, A7, FUNCT_2: 57;

    end;

    

     Lm5: for n,q be Nat, p be Permutation of ( Seg (n + 1)), F,H be FinSequence of ExtREAL st F = (H * p) & q in ( Seg (n + 1)) & ( len H) = (n + 1) & not -infty in ( rng H) & for i be 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, p be Permutation of ( Seg (n + 1)), F,H be FinSequence of ExtREAL ;

      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 be 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));

      

       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: H1 = ((H1 | (q -' 1)) ^ (H1 /^ (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 be Nat st 1 <= i & i <= (q -' 1) holds ((F | (q -' 1)) . i) = ((H1 | (q -' 1)) . i)

      proof

        let i be Nat;

        assume that

         A19: 1 <= i and

         A20: i <= (q -' 1);

        

         A21: ((F | (q -' 1)) . i) = (F . i) by A20, FINSEQ_3: 112;

        

         A22: (H1 . i) = (H . i) by A11, A20, FINSEQ_3: 112, XXREAL_0: 2;

        

         A23: ((H1 | (q -' 1)) . i) = (H1 . 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 thesis by A5, A7, A21, A23, A22, A25, A24;

      end;

      ( 0 + n) <= (1 + n) by XREAL_1: 6;

      then

       A26: ( len H1) = n by A3, FINSEQ_1: 59;

      then

       A27: ( len (H1 | (q -' 1))) = (q -' 1) by A11, FINSEQ_1: 59;

      

       A28: ( len (H1 /^ (q -' 1))) = (n - (q - 1)) by A7, A11, A26, RFINSEQ:def 1;

      for i be Nat st 1 <= i & i <= ((n + 1) - q) holds ((F /^ q) . i) = ((H1 /^ (q -' 1)) . i)

      proof

        reconsider n1 = ((n + 1) - q) as Element of NAT by A10, INT_1: 5;

        let i be Nat;

        assume that

         A29: 1 <= i and

         A30: i <= ((n + 1) - q);

        

         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 (H1 /^ (q -' 1))) by A28, FINSEQ_1:def 3;

        then

         A33: ((H1 /^ (q -' 1)) . i) = (H1 . (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: ((H1 /^ (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 thesis by A5, A37, A34, A36, A38;

      end;

      then

       A39: (F /^ q) = (H1 /^ (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: H1 = (H | ( Seg n)) by FINSEQ_1:def 15;

      then ( rng H1) c= ( rng H) by RELAT_1: 70;

      then not -infty in ( rng H1) by A4;

      then

       A44: not -infty in (( rng (H1 | (q -' 1))) \/ ( rng (H1 /^ (q -' 1)))) by A8, FINSEQ_1: 31;

      then

       A45: not -infty in ( rng (H1 | (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 = (H1 ^ <*(H . (n + 1))*>) by A12, A43, A53, FINSEQ_1: 4, FINSEQ_5: 10;

      

       A55: not -infty in ( rng (H1 /^ (q -' 1))) by A44, XBOOLE_0:def 3;

      

      thus ( Sum F) = (( Sum ((F | (q -' 1)) ^ <*(F . q)*>)) + ( Sum (F /^ q))) by A40, A47, A51, Th8

      .= ((( 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 (H1 | (q -' 1))) + ( Sum (H1 /^ (q -' 1)))) + (H . (n + 1))) by A16, A27, A18, A42, A39, FINSEQ_1: 14

      .= (( Sum H1) + (H . (n + 1))) by A8, A45, A55, Th8

      .= ( Sum H) by A54, Lm1;

    end;

    theorem :: EXTREAL1:11

    for F,G be FinSequence of ExtREAL , s be 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 , s be Permutation of ( dom F);

      defpred P[ Nat] means for F,G be FinSequence of ExtREAL , s be Permutation of ( Seg $1) st ( len F) = $1 & G = (F * s) & not -infty in ( rng F) holds ( Sum F) = ( Sum G);

      

       A1: P[ 0 ]

      proof

        let F,G be FinSequence of ExtREAL , s be Permutation of ( Seg 0 );

        assume that

         A2: ( len F) = 0 and

         A3: G = (F * s);

        F = ( <*> ExtREAL ) by A2;

        hence thesis by A3;

      end;

      

       A4: for n be non zero Nat st P[n] holds P[(n + 1)]

      proof

        let n be non zero Nat;

        assume

         A5: P[n];

        thus P[(n + 1)]

        proof

          let F,G be FinSequence of ExtREAL , s be Permutation of ( Seg (n + 1));

          assume that

           A6: ( len F) = (n + 1) and

           A7: G = (F * s) and

           A8: not -infty in ( rng F);

          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 be Permutation of ( Seg (n + 1)) such that

           A12: for i be 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 be Nat st 1 <= i & i <= n holds ((G | n) . i) = (((H | n) * p1) . i)

            proof

              let i be Nat;

              assume that

               A32: 1 <= i and

               A33: i <= n;

              

               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 thesis by A7, A21, A16, A40, A34, FUNCT_1: 12;

            end;

            ( len (G | n)) = n by A20, A15, FINSEQ_1: 59;

            hence thesis by A30, A31, FINSEQ_1: 14;

          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 thesis by A11, A12, A25, A44, A14, A22, A41, A43, A24, A19, Lm5;

        end;

      end;

      

       A45: P[1]

      proof

        let F,G be FinSequence of ExtREAL , s be Permutation of ( Seg 1);

        assume that

         A46: ( len F) = 1 and

         A47: G = (F * s);

        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 thesis by A51, A49, A50, TARSKI:def 1;

      end;

      

       A52: for n be non zero Nat holds P[n] from NAT_1:sch 10( A45, A4);

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

      then

       A53: P[( len F)] by A1, A52;

      assume that

       A54: G = (F * s) and

       A55: not -infty in ( rng F);

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

      hence thesis by A53, A54, A55;

    end;

    reserve x,y,w,z for ExtReal,

a for Real;

    begin

    theorem :: EXTREAL1:12

    

     Th1: x = a implies |.x.| = |.a qua Complex.|

    proof

      assume

       A1: x = a;

      reconsider x as R_eal by XXREAL_0:def 1;

      per cases ;

        suppose 0 <= x;

        then |.x.| = a by A1, Def1;

        hence thesis by ABSVALUE:def 1;

      end;

        suppose

         A2: not 0 <= x;

        

        then |.x.| = ( - x) by Def1

        .= ( - a) by A1, SUPINF_2: 2;

        hence thesis by A1, A2, ABSVALUE:def 1;

      end;

    end;

    theorem :: EXTREAL1:13

     |.x.| = x or |.x.| = ( - x) by Def1;

    theorem :: EXTREAL1:14

     0 <= |.x.|

    proof

      reconsider x as R_eal by XXREAL_0:def 1;

       0 <= |.x.|;

      hence thesis;

    end;

    theorem :: EXTREAL1:15

    

     Th4: x <> 0 implies 0 < |.x.|

    proof

      assume

       A1: x <> 0 ;

      per cases ;

        suppose 0 <= x;

        hence thesis by A1, Def1;

      end;

        suppose

         A2: not 0 <= x;

        then 0 < ( - x);

        hence thesis by A2, Def1;

      end;

    end;

    theorem :: EXTREAL1:16

    x = 0 iff |.x.| = 0 by Th4, Def1;

    theorem :: EXTREAL1:17

     |.x.| = ( - x) & x <> 0 implies x < 0

    proof

      reconsider x as R_eal by XXREAL_0:def 1;

       0 <= |.x.|;

      hence thesis;

    end;

    theorem :: EXTREAL1:18

    

     Th7: x <= 0 implies |.x.| = ( - x)

    proof

      assume

       A1: x <= 0 ;

      per cases by A1;

        suppose x < 0 ;

        hence thesis by Def1;

      end;

        suppose

         A2: x = 0 ;

        then ( - 0 ) = ( - x);

        hence thesis by A2, Def1;

      end;

    end;

    theorem :: EXTREAL1:19

     |.(x * y).| = ( |.x.| * |.y.|)

    proof

      reconsider x, y as R_eal by XXREAL_0:def 1;

      per cases ;

        suppose x = 0 ;

        then |.x.| = 0 & |.(x * y).| = 0 by Def1;

        hence thesis;

      end;

        suppose

         A1: 0 < x;

        per cases ;

          suppose y = 0 ;

          then |.y.| = 0 & |.(x * y).| = 0 by Def1;

          hence thesis;

        end;

          suppose 0 < y;

          then

           A2: |.y.| = y by Def1;

           |.x.| = x by A1, Def1;

          hence thesis by A2, Def1;

        end;

          suppose

           A3: y < 0 ;

          then

           A4: |.y.| = ( - y) by Def1;

           |.x.| = x by A1, Def1;

          then ( |.x.| * |.y.|) = ( - (x * y)) by A4, XXREAL_3: 92;

          hence thesis by A1, A3, Def1;

        end;

      end;

        suppose

         A5: x < 0 ;

        per cases ;

          suppose y = 0 ;

          then |.y.| = 0 & |.(x * y).| = 0 by Def1;

          hence thesis;

        end;

          suppose

           A6: 0 < y;

          then |.y.| = y by Def1;

          then

           A7: ( |.x.| * |.y.|) = (( - x) * y) by A5, Def1;

           |.(x * y).| = ( - (x * y)) by A5, A6, Def1;

          hence thesis by A7, XXREAL_3: 92;

        end;

          suppose y < 0 ;

          then |.y.| = ( - y) by Def1;

          then ( |.x.| * |.y.|) = (( - x) * ( - y)) by A5, Def1;

          

          then ( |.x.| * |.y.|) = ( - (x * ( - y))) by XXREAL_3: 92

          .= ( - ( - (x * y))) by XXREAL_3: 92;

          hence thesis by Def1;

        end;

      end;

    end;

    theorem :: EXTREAL1:20

    

     Th9: ( - |.x.|) <= x & x <= |.x.|

    proof

      reconsider x as R_eal by XXREAL_0:def 1;

      per cases ;

        suppose

         A1: 0 <= x;

        thus thesis by A1, Def1;

      end;

        suppose not 0 <= x;

        then |.x.| = ( - x) by Def1;

        hence thesis;

      end;

    end;

    theorem :: EXTREAL1:21

    

     Th10: |.x.| < y implies ( - y) < x & x < y

    proof

      assume

       A1: |.x.| < y;

      reconsider x, y as R_eal by XXREAL_0:def 1;

      

       A2: |.x.| < y by A1;

      per cases ;

        suppose 0 <= x;

        hence thesis by A2, Def1;

      end;

        suppose

         A3: not 0 <= x;

        then |.x.| = ( - x) by Def1;

        hence thesis by A1, A3, XXREAL_3: 60;

      end;

    end;

    theorem :: EXTREAL1:22

    

     Th11: ( - y) < x & x < y implies 0 < y & |.x.| < y

    proof

      assume that

       A1: ( - y) < x and

       A2: x < y;

      per cases ;

        suppose 0 <= x;

        hence thesis by A2, Def1;

      end;

        suppose

         A3: not 0 <= x;

        ( - x) < y by A1, XXREAL_3: 60;

        hence thesis by A3, Def1;

      end;

    end;

    theorem :: EXTREAL1:23

    

     Th12: ( - y) <= x & x <= y iff |.x.| <= y

    proof

      

       A1: ( - y) <= x & x <= y implies |.x.| <= y

      proof

        assume that

         A2: ( - y) <= x and

         A3: x <= y;

        per cases ;

          suppose 0 <= x;

          hence thesis by A3, Def1;

        end;

          suppose

           A4: not 0 <= x;

          ( - x) <= y by A2, XXREAL_3: 60;

          hence thesis by A4, Def1;

        end;

      end;

       |.x.| <= y implies ( - y) <= x & x <= y

      proof

        assume

         A5: |.x.| <= y;

        per cases by A5, XXREAL_0: 1;

          suppose |.x.| = y;

          hence thesis by Th9;

        end;

          suppose |.x.| < y;

          hence thesis by Th10;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: EXTREAL1:24

    

     Th13: |.(x + y).| <= ( |.x.| + |.y.|)

    proof

      

       A1: ( - |.x.|) <= x & ( - |.y.|) <= y by Th9;

      

       A2: x <= |.x.| & y <= |.y.| by Th9;

      

       A3: (( - |.x.|) - |.y.|) = ( - ( |.x.| + |.y.|)) by XXREAL_3: 25;

      (x + y) <= ( |.x.| + |.y.|) & (( - |.x.|) + ( - |.y.|)) <= (x + y) by A1, A2, XXREAL_3: 36;

      hence thesis by A3, Th12;

    end;

    theorem :: EXTREAL1:25

    

     Th14: -infty < x & x < +infty & x <> 0 implies ( |.x.| * |.( 1. / x).|) = 1.

    proof

      assume that

       A1: -infty < x & x < +infty and

       A2: x <> 0 ;

      reconsider a = x as Element of REAL by A1, XXREAL_0: 14;

      

       A3: ( 1. / x) = (1 / a);

      per cases ;

        suppose 0 <= x;

        then |.x.| = a & |.( 1. / x).| = (1 / a) by Def1;

        then ( |.x.| * |.( 1. / x).|) = (a * (1 / a)) by XXREAL_3:def 5;

        hence thesis by A2, XCMPLX_1: 106;

      end;

        suppose

         A4: not 0 <= x;

        

        then

         A5: |.x.| = ( - x) by Def1

        .= ( - a) by SUPINF_2: 2;

         |.( 1. / x).| = ( - ( 1. / x)) by A3, A4, Def1

        .= ( - (1 / a));

        

        then ( |.x.| * |.( 1. / x).|) = (( - a) * ( - (1 / a))) by A5, XXREAL_3:def 5

        .= (a * (1 / a));

        hence thesis by A4, XCMPLX_1: 106;

      end;

    end;

    theorem :: EXTREAL1:26

    x = +infty or x = -infty implies ( |.x.| * |.( 1. / x).|) = 0

    proof

      assume x = +infty or x = -infty ;

      then |.( 1. / x).| = 0 by Def1;

      hence thesis;

    end;

    theorem :: EXTREAL1:27

    x <> 0 implies |.( 1. / x).| = ( 1. / |.x.|)

    proof

      assume

       A1: x <> 0 ;

      per cases ;

        suppose

         A2: x = +infty ;

        then |.( 1. / x).| = 0 by Def1;

        hence thesis by A2, Def1;

      end;

        suppose x = -infty ;

        then |.( 1. / x).| = 0 & |.x.| = +infty by Def1, XXREAL_3: 5;

        hence thesis;

      end;

        suppose

         A3: x <> +infty & x <> -infty ;

        

         A4: 0 < |.x.| by A1, Th4;

        

         A5: x < +infty by A3, XXREAL_0: 4;

         -infty <= x by XXREAL_0: 5;

        then

         A6: -infty < x by A3, XXREAL_0: 1;

        then ( - +infty ) < x by XXREAL_3:def 3;

        then

         A7: |.x.| < +infty by A5, Th11;

        ( |.( 1. / x).| * |.x.|) = 1. by A1, A6, A5, Th14;

        hence thesis by A4, A7, XXREAL_3: 88;

      end;

    end;

    theorem :: EXTREAL1:28

     not ((x = -infty or x = +infty ) & (y = -infty or y = +infty )) & y <> 0 implies |.(x / y).| = ( |.x.| / |.y.|)

    proof

      assume that

       A1: not ((x = -infty or x = +infty ) & (y = -infty or y = +infty )) and

       A2: y <> 0 ;

      reconsider y as R_eal by XXREAL_0:def 1;

      per cases ;

        suppose

         A3: x = +infty ;

        

         A4: -infty < y by A1, A3, XXREAL_0: 12, XXREAL_0: 14;

        per cases by A2;

          suppose

           A5: 0 < y;

          then (x / y) = +infty by A3, A1, XXREAL_3: 83;

          then

           A6: |.(x / y).| = +infty by Def1;

           |.y.| = y by A5, Def1;

          hence thesis by A3, A1, A5, A6, XXREAL_3: 83;

        end;

          suppose

           A7: y < 0 ;

          then |.y.| = ( - y) by Def1;

          then

           A8: |.y.| < +infty by A4, XXREAL_3: 5, XXREAL_3: 38;

          (x / y) = -infty by A3, A1, A7, XXREAL_3: 85;

          then |.(x / y).| = +infty by Def1, XXREAL_3: 5;

          hence thesis by A8, A2, A3, Th4, XXREAL_3: 83;

        end;

      end;

        suppose

         A9: x = -infty ;

        

         A10: -infty < y by A1, A9, XXREAL_0: 12, XXREAL_0: 14;

        per cases by A2;

          suppose

           A11: 0 < y;

          then

           A12: (x / y) = -infty by A9, A1, XXREAL_3: 86;

          

           A13: |.x.| = +infty by A9, Def1, XXREAL_3: 5;

           |.y.| = y by A11, Def1;

          hence thesis by A9, A1, A11, A12, A13, XXREAL_3: 83;

        end;

          suppose

           A14: y < 0 ;

          then |.y.| = ( - y) by Def1;

          then

           A15: |.y.| < +infty by A10, XXREAL_3: 5, XXREAL_3: 38;

          

           A16: (x / y) = +infty by A9, A1, A14, XXREAL_3: 84;

           0 < |.y.| & |.x.| = +infty by A2, A9, Th4, Def1, XXREAL_3: 5;

          hence thesis by A15, A16, XXREAL_3: 83;

        end;

      end;

        suppose x <> +infty & x <> -infty ;

        then

        reconsider a = x as Element of REAL by XXREAL_0: 14;

        per cases ;

          suppose y = +infty ;

          then |.(x / y).| = 0 & |.y.| = +infty by Def1;

          hence thesis;

        end;

          suppose y = -infty ;

          then |.(x / y).| = 0 & |.y.| = +infty by Def1, XXREAL_3: 5;

          hence thesis;

        end;

          suppose y <> +infty & y <> -infty ;

          then

          reconsider b = y as Element of REAL by XXREAL_0: 14;

           |.x.| = |.a qua Complex.| & |.y.| = |.b qua Complex.| by Th1;

          then

           A17: ( |.x.| / |.y.|) = ( |.a qua Complex.| / |.b qua Complex.|);

           |.(x / y).| = |.(a / b) qua Complex.| by Th1;

          hence thesis by A17, COMPLEX1: 67;

        end;

      end;

    end;

    theorem :: EXTREAL1:29

    

     Th18: |.x.| = |.( - x).|

    proof

      reconsider x as R_eal by XXREAL_0:def 1;

      per cases ;

        suppose 0 < x;

        

        then |.( - x).| = ( - ( - x)) by Def1

        .= x;

        hence thesis;

      end;

        suppose x < 0 ;

        then |.x.| = ( - x) by Def1;

        hence thesis;

      end;

        suppose x = 0 ;

        hence thesis;

      end;

    end;

    theorem :: EXTREAL1:30

    

     Th19: |. +infty .| = +infty & |. -infty .| = +infty

    proof

      thus |. +infty .| = +infty by Def1;

      ( - -infty ) = +infty by XXREAL_3: 23;

      hence thesis by Def1;

    end;

    theorem :: EXTREAL1:31

    

     Th20: x is Real or y is Real implies ( |.x.| - |.y.|) <= |.(x - y).|

    proof

      assume

       A1: x is Real or y is Real;

      reconsider x, y as R_eal by XXREAL_0:def 1;

      per cases by A1;

        suppose y is Real;

        then ((x - y) + y) = x by XXREAL_3: 22;

        then |.x.| <= ( |.(x - y).| + |.y.|) by Th13;

        hence thesis by XXREAL_3: 42;

      end;

        suppose x is Real;

        then

        reconsider a = x as Real;

        

         A2: |.x.| = |.a.|;

        per cases ;

          suppose

           A3: y = +infty or y = -infty ;

           |.y.| = +infty by Th19, A3;

          then ( |.x.| - |.y.|) = -infty by A2, XXREAL_3: 13;

          then ( |.x.| - |.y.|) <= |.(x - y).|;

          hence thesis;

        end;

          suppose y <> +infty & y <> -infty ;

          then

          reconsider b = y as Element of REAL by XXREAL_0: 14;

          (x - y) = (a - b) by SUPINF_2: 3;

          then

           A4: |.(x - y).| = |.(a - b) qua Complex.| by Th1;

           |.y.| = |.b qua Complex.| by Th1;

          then ( |.x.| - |.y.|) = ( |.a qua Complex.| - |.b qua Complex.|) by A2, SUPINF_2: 3;

          hence thesis by A4, COMPLEX1: 59;

        end;

      end;

    end;

    theorem :: EXTREAL1:32

     |.(x - y).| <= ( |.x.| + |.y.|)

    proof

      reconsider x, y as R_eal by XXREAL_0:def 1;

      per cases ;

        suppose x = +infty or x = -infty ;

        then ( |.x.| + |.y.|) = +infty by Th19, XXREAL_3:def 2;

        hence thesis by XXREAL_0: 3;

      end;

        suppose

         A1: x <> +infty & x <> -infty ;

        then

        reconsider a = x as Element of REAL by XXREAL_0: 14;

        per cases ;

          suppose

           A2: y = +infty ;

          (x - y) = -infty by A1, A2, XXREAL_3: 13;

          hence thesis by A2, Th19, XXREAL_3:def 2;

        end;

          suppose

           A3: y = -infty ;

          (x - y) = +infty by A1, A3, XXREAL_3: 14;

          hence thesis by A3, Th19, XXREAL_3:def 2;

        end;

          suppose y <> +infty & y <> -infty ;

          then

          reconsider b = y as Element of REAL by XXREAL_0: 14;

           |.x.| = |.a qua Complex.| & |.y.| = |.b qua Complex.| by Th1;

          then

           A4: ( |.x.| + |.y.|) = ( |.a qua Complex.| + |.b qua Complex.|) by SUPINF_2: 1;

          (x - y) = (a - b) by SUPINF_2: 3;

          then |.(x - y).| = |.(a - b) qua Complex.| by Th1;

          hence thesis by A4, COMPLEX1: 57;

        end;

      end;

    end;

    ::$Canceled

    theorem :: EXTREAL1:34

     |.x.| <= z & |.y.| <= w implies |.(x + y).| <= (z + w)

    proof

      assume

       A1: |.x.| <= z & |.y.| <= w;

      then ( - z) <= x & ( - w) <= y by Th12;

      then

       A2: (( - z) + ( - w)) <= (x + y) by XXREAL_3: 36;

      x <= z & y <= w by A1, Th12;

      then

       A3: (x + y) <= (z + w) by XXREAL_3: 36;

      (( - z) - w) = ( - (z + w)) by XXREAL_3: 25;

      hence thesis by A3, A2, Th12;

    end;

    theorem :: EXTREAL1:35

    x is Real or y is Real implies |.( |.x.| - |.y.|).| <= |.(x - y).|

    proof

      

       A1: ( |.y.| - |.x.|) = ( - ( |.x.| - |.y.|)) by XXREAL_3: 26;

      assume

       A2: x is Real or y is Real;

      then

       A3: ( |.x.| - |.y.|) <= |.(x - y).| by Th20;

      (y - x) = ( - (x - y)) by XXREAL_3: 26;

      then

       A4: |.(y - x).| = |.(x - y).| by Th18;

      ( |.y.| - |.x.|) <= |.(y - x).| by A2, Th20;

      then ( - |.(x - y).|) <= ( - ( - ( |.x.| - |.y.|))) by A4, A1, XXREAL_3: 38;

      hence thesis by A3, Th12;

    end;

    theorem :: EXTREAL1:36

     0 <= (x * y) implies |.(x + y).| = ( |.x.| + |.y.|)

    proof

      assume

       A1: 0 <= (x * y);

      per cases by A1;

        suppose ( 0 <= x or 0 < x) & ( 0 <= y or 0 < y);

        then |.x.| = x & |.y.| = y by Def1;

        hence thesis by Def1;

      end;

        suppose

         A2: (x <= 0 or x < 0 ) & (y <= 0 or y < 0 );

        

        then

         A3: |.(x + y).| = ( - (x + y)) by Th7

        .= (( - x) - y) by XXREAL_3: 25;

         |.x.| = ( - x) by A2, Th7;

        hence thesis by A2, A3, Th7;

      end;

    end;

    begin

    theorem :: EXTREAL1:37

    x <> +infty & y <> +infty & not (x = +infty & y = +infty or x = -infty & y = -infty ) implies ( min (x,y)) = (((x + y) - |.(x - y).|) / 2)

    proof

      assume that

       A1: x <> +infty and

       A2: y <> +infty and

       A3: not (x = +infty & y = +infty or x = -infty & y = -infty );

      per cases ;

        suppose

         A4: x = -infty ;

        then (x + y) = -infty & (x - y) = -infty by A2, A3, XXREAL_3: 14, XXREAL_3:def 2;

        then

         A5: ((x + y) - |.(x - y).|) = -infty by XXREAL_3: 14;

        

         A6: ( min (x,y)) = -infty by A4, XXREAL_0: 44;

        thus thesis by A6, A5, XXREAL_3: 86;

      end;

        suppose x <> -infty ;

        then

        reconsider a = x as Element of REAL by A1, XXREAL_0: 14;

        per cases ;

          suppose

           A7: y = -infty ;

          then (x + y) = -infty & (x - y) = +infty by A1, A3, XXREAL_3: 14, XXREAL_3:def 2;

          then

           A8: ((x + y) - |.(x - y).|) = -infty by XXREAL_3: 14;

          

           A9: ( min (x,y)) = -infty by A7, XXREAL_0: 44;

          thus thesis by A9, A8, XXREAL_3: 86;

        end;

          suppose y <> -infty ;

          then

          reconsider b = y as Element of REAL by A2, XXREAL_0: 14;

          (x - y) = (a - b) by SUPINF_2: 3;

          then (x + y) = (a + b) & |.(x - y).| = |.(a - b).| by SUPINF_2: 1;

          then

           A10: ((x + y) - |.(x - y).|) = ((a + b) - |.(a - b) qua Complex.|) by SUPINF_2: 3;

          (((x + y) - |.(x - y).|) / 2) = (((a + b) - |.(a - b) qua Complex.|) / 2) by A10;

          hence thesis by COMPLEX1: 73;

        end;

      end;

    end;

    theorem :: EXTREAL1:38

    x <> -infty & y <> -infty & not (x = +infty & y = +infty or x = -infty & y = -infty ) implies ( max (x,y)) = (((x + y) + |.(x - y).|) / 2)

    proof

      assume that

       A1: x <> -infty and

       A2: y <> -infty and

       A3: not (x = +infty & y = +infty or x = -infty & y = -infty );

      per cases ;

        suppose

         A4: x = +infty ;

        then (x + y) = +infty & (x - y) = +infty by A2, A3, XXREAL_3: 13, XXREAL_3:def 2;

        then

         A5: ((x + y) + |.(x - y).|) = +infty by XXREAL_3:def 2;

        

         A6: ( max (x,y)) = +infty by A4, XXREAL_0: 41;

        thus thesis by A6, A5, XXREAL_3: 83;

      end;

        suppose x <> +infty ;

        then

        reconsider a = x as Element of REAL by A1, XXREAL_0: 14;

        per cases ;

          suppose

           A7: y = +infty ;

          then (x + y) = +infty & (x - y) = -infty by A1, A3, XXREAL_3: 13, XXREAL_3:def 2;

          then

           A8: ((x + y) + |.(x - y).|) = +infty by XXREAL_3:def 2;

          

           A9: ( max (x,y)) = +infty by A7, XXREAL_0: 41;

          thus thesis by A9, A8, XXREAL_3: 83;

        end;

          suppose y <> +infty ;

          then

          reconsider b = y as Element of REAL by A2, XXREAL_0: 14;

          (x - y) = (a - b) by SUPINF_2: 3;

          then (x + y) = (a + b) & |.(x - y).| = |.(a - b).| by SUPINF_2: 1;

          then

           A10: ((x + y) + |.(x - y).|) = ((a + b) + |.(a - b) qua Complex.|) by SUPINF_2: 1;

          (((x + y) + |.(x - y).|) / 2) = (((a + b) + |.(a - b) qua Complex.|) / 2) by A10;

          hence thesis by COMPLEX1: 74;

        end;

      end;

    end;

    definition

      let x,y be R_eal;

      :: original: max

      redefine

      func max (x,y) -> R_eal ;

      coherence by XXREAL_0:def 1;

      :: original: min

      redefine

      func min (x,y) -> R_eal ;

      coherence by XXREAL_0:def 1;

    end

    theorem :: EXTREAL1:39

    (( min (x,y)) + ( max (x,y))) = (x + y)

    proof

      per cases ;

        suppose

         A1: x <= y;

        then ( min (x,y)) = x by XXREAL_0:def 9;

        hence thesis by A1, XXREAL_0:def 10;

      end;

        suppose

         A2: not x <= y;

        then ( min (x,y)) = y by XXREAL_0:def 9;

        hence thesis by A2, XXREAL_0:def 10;

      end;

    end;

    begin

    theorem :: EXTREAL1:40

    

     Th28: |.x.| = +infty implies x = +infty or x = -infty

    proof

      

       A1: |.x.| = x or ( - |.x.|) = ( - ( - x)) by Def1;

      assume |.x.| = +infty ;

      hence thesis by A1, XXREAL_3: 5;

    end;

    theorem :: EXTREAL1:41

     |.x.| < +infty iff x in REAL by Th19, Th28, XXREAL_0: 4, XXREAL_0: 14;