valued_0.miz



    begin

    definition

      let f be Relation;

      :: VALUED_0:def1

      attr f is complex-valued means

      : Def1: ( rng f) c= COMPLEX ;

      :: VALUED_0:def2

      attr f is ext-real-valued means

      : Def2: ( rng f) c= ExtREAL ;

      :: VALUED_0:def3

      attr f is real-valued means

      : Def3: ( rng f) c= REAL ;

      ::$Canceled

      :: VALUED_0:def6

      attr f is natural-valued means

      : Def4: ( rng f) c= NAT ;

    end

    registration

      cluster natural-valued -> INT -valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= NAT ;

        hence ( rng R) c= INT by NUMBERS: 17;

      end;

      cluster INT -valued -> RAT -valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= INT ;

        hence ( rng R) c= RAT by NUMBERS: 14;

      end;

      cluster INT -valued -> real-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= INT ;

        hence ( rng R) c= REAL by NUMBERS: 15;

      end;

      cluster RAT -valued -> real-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= RAT ;

        hence ( rng R) c= REAL by NUMBERS: 12;

      end;

      cluster real-valued -> ext-real-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= REAL ;

        hence ( rng R) c= ExtREAL by NUMBERS: 31;

      end;

      cluster real-valued -> complex-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= REAL ;

        hence ( rng R) c= COMPLEX by NUMBERS: 11;

      end;

      cluster natural-valued -> RAT -valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= NAT ;

        hence ( rng R) c= RAT by NUMBERS: 18;

      end;

      cluster natural-valued -> real-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume ( rng R) c= NAT ;

        hence ( rng R) c= REAL by NUMBERS: 19;

      end;

    end

    registration

      cluster empty -> natural-valued for Relation;

      coherence

      proof

        let R be Relation;

        assume R is empty;

        hence ( rng R) c= NAT ;

      end;

    end

    registration

      cluster natural-valued for Function;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let R be complex-valued Relation;

      cluster ( rng R) -> complex-membered;

      coherence

      proof

        ( rng R) c= COMPLEX by Def1;

        hence thesis;

      end;

    end

    registration

      let R be ext-real-valued Relation;

      cluster ( rng R) -> ext-real-membered;

      coherence

      proof

        ( rng R) c= ExtREAL by Def2;

        hence thesis;

      end;

    end

    registration

      let R be real-valued Relation;

      cluster ( rng R) -> real-membered;

      coherence

      proof

        ( rng R) c= REAL by Def3;

        hence thesis;

      end;

    end

    registration

      let R be RAT -valued Relation;

      cluster ( rng R) -> rational-membered;

      coherence ;

    end

    registration

      let R be INT -valued Relation;

      cluster ( rng R) -> integer-membered;

      coherence ;

    end

    registration

      let R be natural-valued Relation;

      cluster ( rng R) -> natural-membered;

      coherence

      proof

        ( rng R) c= NAT by Def4;

        hence thesis;

      end;

    end

    reserve x,y for object,

X for set,

f for Function,

R,S for Relation;

    theorem :: VALUED_0:1

    

     Th1: for S be complex-valued Relation st R c= S holds R is complex-valued

    proof

      let S be complex-valued Relation;

      assume R c= S;

      then

       A1: ( rng R) c= ( rng S) by RELAT_1: 11;

      ( rng S) c= COMPLEX by Def1;

      hence ( rng R) c= COMPLEX by A1;

    end;

    theorem :: VALUED_0:2

    

     Th2: for S be ext-real-valued Relation st R c= S holds R is ext-real-valued

    proof

      let S be ext-real-valued Relation;

      assume R c= S;

      then

       A1: ( rng R) c= ( rng S) by RELAT_1: 11;

      ( rng S) c= ExtREAL by Def2;

      hence ( rng R) c= ExtREAL by A1;

    end;

    theorem :: VALUED_0:3

    

     Th3: for S be real-valued Relation st R c= S holds R is real-valued

    proof

      let S be real-valued Relation;

      assume R c= S;

      then

       A1: ( rng R) c= ( rng S) by RELAT_1: 11;

      ( rng S) c= REAL by Def3;

      hence ( rng R) c= REAL by A1;

    end;

    theorem :: VALUED_0:4

    for S be RAT -valued Relation st R c= S holds R is RAT -valued;

    theorem :: VALUED_0:5

    for S be INT -valued Relation st R c= S holds R is INT -valued;

    theorem :: VALUED_0:6

    

     Th6: for S be natural-valued Relation st R c= S holds R is natural-valued

    proof

      let S be natural-valued Relation;

      assume R c= S;

      then

       A1: ( rng R) c= ( rng S) by RELAT_1: 11;

      ( rng S) c= NAT by Def4;

      hence ( rng R) c= NAT by A1;

    end;

    registration

      let R be complex-valued Relation;

      cluster -> complex-valued for Subset of R;

      coherence by Th1;

    end

    registration

      let R be ext-real-valued Relation;

      cluster -> ext-real-valued for Subset of R;

      coherence by Th2;

    end

    registration

      let R be real-valued Relation;

      cluster -> real-valued for Subset of R;

      coherence by Th3;

    end

    registration

      let R be RAT -valued Relation;

      cluster -> RAT -valued for Subset of R;

      coherence ;

    end

    registration

      let R be INT -valued Relation;

      cluster -> INT -valued for Subset of R;

      coherence ;

    end

    registration

      let R be natural-valued Relation;

      cluster -> natural-valued for Subset of R;

      coherence by Th6;

    end

    registration

      let R,S be complex-valued Relation;

      cluster (R \/ S) -> complex-valued;

      coherence

      proof

        

         A1: ( rng (R \/ S)) = (( rng R) \/ ( rng S)) by RELAT_1: 12;

        ( rng R) c= COMPLEX & ( rng S) c= COMPLEX by Def1;

        hence ( rng (R \/ S)) c= COMPLEX by A1, XBOOLE_1: 8;

      end;

    end

    registration

      let R,S be ext-real-valued Relation;

      cluster (R \/ S) -> ext-real-valued;

      coherence

      proof

        

         A1: ( rng (R \/ S)) = (( rng R) \/ ( rng S)) by RELAT_1: 12;

        ( rng R) c= ExtREAL & ( rng S) c= ExtREAL by Def2;

        hence ( rng (R \/ S)) c= ExtREAL by A1, XBOOLE_1: 8;

      end;

    end

    registration

      let R,S be real-valued Relation;

      cluster (R \/ S) -> real-valued;

      coherence

      proof

        

         A1: ( rng (R \/ S)) = (( rng R) \/ ( rng S)) by RELAT_1: 12;

        ( rng R) c= REAL & ( rng S) c= REAL by Def3;

        hence ( rng (R \/ S)) c= REAL by A1, XBOOLE_1: 8;

      end;

    end

    registration

      let R,S be RAT -valued Relation;

      cluster (R \/ S) -> RAT -valued;

      coherence ;

    end

    registration

      let R,S be INT -valued Relation;

      cluster (R \/ S) -> INT -valued;

      coherence ;

    end

    registration

      let R,S be natural-valued Relation;

      cluster (R \/ S) -> natural-valued;

      coherence

      proof

        

         A1: ( rng (R \/ S)) = (( rng R) \/ ( rng S)) by RELAT_1: 12;

        ( rng R) c= NAT & ( rng S) c= NAT by Def4;

        hence ( rng (R \/ S)) c= NAT by A1, XBOOLE_1: 8;

      end;

    end

    registration

      let R be complex-valued Relation;

      let S;

      cluster (R /\ S) -> complex-valued;

      coherence

      proof

        (R /\ S) c= R by XBOOLE_1: 17;

        then

         A1: ( rng (R /\ S)) c= ( rng R) by RELAT_1: 11;

        ( rng R) c= COMPLEX by Def1;

        hence ( rng (R /\ S)) c= COMPLEX by A1;

      end;

      cluster (R \ S) -> complex-valued;

      coherence ;

    end

    registration

      let R be ext-real-valued Relation;

      let S;

      cluster (R /\ S) -> ext-real-valued;

      coherence

      proof

        (R /\ S) c= R by XBOOLE_1: 17;

        then

         A1: ( rng (R /\ S)) c= ( rng R) by RELAT_1: 11;

        ( rng R) c= ExtREAL by Def2;

        hence ( rng (R /\ S)) c= ExtREAL by A1;

      end;

      cluster (R \ S) -> ext-real-valued;

      coherence ;

    end

    registration

      let R be real-valued Relation;

      let S;

      cluster (R /\ S) -> real-valued;

      coherence

      proof

        (R /\ S) c= R by XBOOLE_1: 17;

        then

         A1: ( rng (R /\ S)) c= ( rng R) by RELAT_1: 11;

        ( rng R) c= REAL by Def3;

        hence ( rng (R /\ S)) c= REAL by A1;

      end;

      cluster (R \ S) -> real-valued;

      coherence ;

    end

    registration

      let R be RAT -valued Relation;

      let S;

      cluster (R /\ S) -> RAT -valued;

      coherence ;

      cluster (R \ S) -> RAT -valued;

      coherence ;

    end

    registration

      let R be INT -valued Relation;

      let S;

      cluster (R /\ S) -> INT -valued;

      coherence ;

      cluster (R \ S) -> INT -valued;

      coherence ;

    end

    registration

      let R be natural-valued Relation;

      let S;

      cluster (R /\ S) -> natural-valued;

      coherence

      proof

        (R /\ S) c= R by XBOOLE_1: 17;

        then

         A1: ( rng (R /\ S)) c= ( rng R) by RELAT_1: 11;

        ( rng R) c= NAT by Def4;

        hence ( rng (R /\ S)) c= NAT by A1;

      end;

      cluster (R \ S) -> natural-valued;

      coherence ;

    end

    registration

      let R,S be complex-valued Relation;

      cluster (R \+\ S) -> complex-valued;

      coherence ;

    end

    registration

      let R,S be ext-real-valued Relation;

      cluster (R \+\ S) -> ext-real-valued;

      coherence ;

    end

    registration

      let R,S be real-valued Relation;

      cluster (R \+\ S) -> real-valued;

      coherence ;

    end

    registration

      let R,S be RAT -valued Relation;

      cluster (R \+\ S) -> RAT -valued;

      coherence ;

    end

    registration

      let R,S be INT -valued Relation;

      cluster (R \+\ S) -> INT -valued;

      coherence ;

    end

    registration

      let R,S be natural-valued Relation;

      cluster (R \+\ S) -> natural-valued;

      coherence ;

    end

    registration

      let R be complex-valued Relation;

      let X;

      cluster (R .: X) -> complex-membered;

      coherence

      proof

        (R .: X) c= ( rng R) by RELAT_1: 111;

        hence thesis;

      end;

    end

    registration

      let R be ext-real-valued Relation;

      let X;

      cluster (R .: X) -> ext-real-membered;

      coherence

      proof

        (R .: X) c= ( rng R) by RELAT_1: 111;

        hence thesis;

      end;

    end

    registration

      let R be real-valued Relation;

      let X;

      cluster (R .: X) -> real-membered;

      coherence

      proof

        (R .: X) c= ( rng R) by RELAT_1: 111;

        hence thesis;

      end;

    end

    registration

      let R be RAT -valued Relation;

      let X;

      cluster (R .: X) -> rational-membered;

      coherence

      proof

        (R .: X) c= ( rng R) by RELAT_1: 111;

        hence thesis;

      end;

    end

    registration

      let R be INT -valued Relation;

      let X;

      cluster (R .: X) -> integer-membered;

      coherence

      proof

        (R .: X) c= ( rng R) by RELAT_1: 111;

        hence thesis;

      end;

    end

    registration

      let R be natural-valued Relation;

      let X;

      cluster (R .: X) -> natural-membered;

      coherence

      proof

        (R .: X) c= ( rng R) by RELAT_1: 111;

        hence thesis;

      end;

    end

    registration

      let R be complex-valued Relation;

      let x;

      cluster ( Im (R,x)) -> complex-membered;

      coherence ;

    end

    registration

      let R be ext-real-valued Relation;

      let x;

      cluster ( Im (R,x)) -> ext-real-membered;

      coherence ;

    end

    registration

      let R be real-valued Relation;

      let x;

      cluster ( Im (R,x)) -> real-membered;

      coherence ;

    end

    registration

      let R be RAT -valued Relation;

      let x;

      cluster ( Im (R,x)) -> rational-membered;

      coherence ;

    end

    registration

      let R be INT -valued Relation;

      let x;

      cluster ( Im (R,x)) -> integer-membered;

      coherence ;

    end

    registration

      let R be natural-valued Relation;

      let x;

      cluster ( Im (R,x)) -> natural-membered;

      coherence ;

    end

    registration

      let R be complex-valued Relation;

      let X;

      cluster (R | X) -> complex-valued;

      coherence

      proof

        ( rng R) c= COMPLEX & ( rng (R | X)) c= ( rng R) by Def1, RELAT_1: 70;

        hence ( rng (R | X)) c= COMPLEX ;

      end;

    end

    registration

      let R be ext-real-valued Relation;

      let X;

      cluster (R | X) -> ext-real-valued;

      coherence

      proof

        ( rng R) c= ExtREAL & ( rng (R | X)) c= ( rng R) by Def2, RELAT_1: 70;

        hence ( rng (R | X)) c= ExtREAL ;

      end;

    end

    registration

      let R be real-valued Relation;

      let X;

      cluster (R | X) -> real-valued;

      coherence

      proof

        ( rng R) c= REAL & ( rng (R | X)) c= ( rng R) by Def3, RELAT_1: 70;

        hence ( rng (R | X)) c= REAL ;

      end;

    end

    registration

      let R be RAT -valued Relation;

      let X;

      cluster (R | X) -> RAT -valued;

      coherence ;

    end

    registration

      let R be INT -valued Relation;

      let X;

      cluster (R | X) -> INT -valued;

      coherence ;

    end

    registration

      let R be natural-valued Relation;

      let X;

      cluster (R | X) -> natural-valued;

      coherence

      proof

        ( rng R) c= NAT & ( rng (R | X)) c= ( rng R) by Def4, RELAT_1: 70;

        hence ( rng (R | X)) c= NAT ;

      end;

    end

    registration

      let X be complex-membered set;

      cluster ( id X) -> complex-valued;

      coherence by MEMBERED: 1;

    end

    registration

      let X be ext-real-membered set;

      cluster ( id X) -> ext-real-valued;

      coherence by MEMBERED: 2;

    end

    registration

      let X be real-membered set;

      cluster ( id X) -> real-valued;

      coherence by MEMBERED: 3;

    end

    registration

      let X be rational-membered set;

      cluster ( id X) -> RAT -valued;

      coherence by MEMBERED: 4;

    end

    registration

      let X be integer-membered set;

      cluster ( id X) -> INT -valued;

      coherence by MEMBERED: 5;

    end

    registration

      let X be natural-membered set;

      cluster ( id X) -> natural-valued;

      coherence by MEMBERED: 6;

    end

    registration

      let R;

      let S be complex-valued Relation;

      cluster (R * S) -> complex-valued;

      coherence

      proof

        ( rng S) c= COMPLEX & ( rng (R * S)) c= ( rng S) by Def1, RELAT_1: 26;

        hence ( rng (R * S)) c= COMPLEX ;

      end;

    end

    registration

      let R;

      let S be ext-real-valued Relation;

      cluster (R * S) -> ext-real-valued;

      coherence

      proof

        ( rng S) c= ExtREAL & ( rng (R * S)) c= ( rng S) by Def2, RELAT_1: 26;

        hence ( rng (R * S)) c= ExtREAL ;

      end;

    end

    registration

      let R;

      let S be real-valued Relation;

      cluster (R * S) -> real-valued;

      coherence

      proof

        ( rng S) c= REAL & ( rng (R * S)) c= ( rng S) by Def3, RELAT_1: 26;

        hence ( rng (R * S)) c= REAL ;

      end;

    end

    registration

      let R;

      let S be RAT -valued Relation;

      cluster (R * S) -> RAT -valued;

      coherence ;

    end

    registration

      let R;

      let S be INT -valued Relation;

      cluster (R * S) -> INT -valued;

      coherence ;

    end

    registration

      let R;

      let S be natural-valued Relation;

      cluster (R * S) -> natural-valued;

      coherence

      proof

        ( rng S) c= NAT & ( rng (R * S)) c= ( rng S) by Def4, RELAT_1: 26;

        hence ( rng (R * S)) c= NAT ;

      end;

    end

    definition

      let f be Function;

      :: original: complex-valued

      redefine

      :: VALUED_0:def7

      attr f is complex-valued means for x st x in ( dom f) holds (f . x) is complex;

      compatibility

      proof

        thus f is complex-valued implies for x st x in ( dom f) holds (f . x) is complex

        proof

          assume

           A1: f is complex-valued;

          let x;

          assume

           A2: x in ( dom f);

          reconsider f as complex-valued Function by A1;

          (f . x) in ( rng f) by A2, FUNCT_1: 3;

          hence thesis;

        end;

        assume

         A3: for x st x in ( dom f) holds (f . x) is complex;

        let y be object;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        then y is complex by A3;

        hence thesis by XCMPLX_0:def 2;

      end;

      :: original: ext-real-valued

      redefine

      :: VALUED_0:def8

      attr f is ext-real-valued means for x st x in ( dom f) holds (f . x) is ext-real;

      compatibility

      proof

        thus f is ext-real-valued implies for x st x in ( dom f) holds (f . x) is ext-real

        proof

          assume

           A4: f is ext-real-valued;

          let x;

          assume

           A5: x in ( dom f);

          reconsider f as ext-real-valued Function by A4;

          (f . x) in ( rng f) by A5, FUNCT_1: 3;

          hence thesis;

        end;

        assume

         A6: for x st x in ( dom f) holds (f . x) is ext-real;

        let y be object;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        then y is ext-real by A6;

        hence thesis by XXREAL_0:def 1;

      end;

      :: original: real-valued

      redefine

      :: VALUED_0:def9

      attr f is real-valued means for x st x in ( dom f) holds (f . x) is real;

      compatibility

      proof

        thus f is real-valued implies for x st x in ( dom f) holds (f . x) is real

        proof

          assume

           A7: f is real-valued;

          let x;

          assume

           A8: x in ( dom f);

          reconsider f as real-valued Function by A7;

          (f . x) in ( rng f) by A8, FUNCT_1: 3;

          hence thesis;

        end;

        assume

         A9: for x st x in ( dom f) holds (f . x) is real;

        let y be object;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        then y is real by A9;

        hence thesis by XREAL_0:def 1;

      end;

      ::$Canceled

      :: original: natural-valued

      redefine

      :: VALUED_0:def12

      attr f is natural-valued means for x st x in ( dom f) holds (f . x) is natural;

      compatibility

      proof

        thus f is natural-valued implies for x st x in ( dom f) holds (f . x) is natural

        proof

          assume

           A10: f is natural-valued;

          let x;

          assume

           A11: x in ( dom f);

          reconsider f as natural-valued Function by A10;

          (f . x) in ( rng f) by A11, FUNCT_1: 3;

          hence thesis;

        end;

        assume

         A12: for x st x in ( dom f) holds (f . x) is natural;

        let y be object;

        assume y in ( rng f);

        then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        then y is natural by A12;

        hence thesis by ORDINAL1:def 12;

      end;

    end

    theorem :: VALUED_0:7

    

     Th7: f is complex-valued iff for x holds (f . x) is complex

    proof

      hereby

        assume

         A1: f is complex-valued;

        let x;

        per cases ;

          suppose x in ( dom f);

          hence (f . x) is complex by A1;

        end;

          suppose not x in ( dom f);

          hence (f . x) is complex by FUNCT_1:def 2;

        end;

      end;

      assume for x holds (f . x) is complex;

      then for x st x in ( dom f) holds (f . x) is complex;

      hence thesis;

    end;

    theorem :: VALUED_0:8

    

     Th8: f is ext-real-valued iff for x holds (f . x) is ext-real

    proof

      hereby

        assume

         A1: f is ext-real-valued;

        let x;

        per cases ;

          suppose x in ( dom f);

          hence (f . x) is ext-real by A1;

        end;

          suppose not x in ( dom f);

          hence (f . x) is ext-real by FUNCT_1:def 2;

        end;

      end;

      assume for x holds (f . x) is ext-real;

      then for x st x in ( dom f) holds (f . x) is ext-real;

      hence thesis;

    end;

    theorem :: VALUED_0:9

    

     Th9: f is real-valued iff for x holds (f . x) is real

    proof

      hereby

        assume

         A1: f is real-valued;

        let x;

        per cases ;

          suppose x in ( dom f);

          hence (f . x) is real by A1;

        end;

          suppose not x in ( dom f);

          hence (f . x) is real by FUNCT_1:def 2;

        end;

      end;

      assume for x holds (f . x) is real;

      then for x st x in ( dom f) holds (f . x) is real;

      hence thesis;

    end;

    theorem :: VALUED_0:10

    

     Th10: f is RAT -valued iff for x holds (f . x) is rational

    proof

      hereby

        assume

         A1: f is RAT -valued;

        let x;

        per cases ;

          suppose x in ( dom f);

          then (f . x) in ( rng f) by FUNCT_1:def 3;

          hence (f . x) is rational by A1;

        end;

          suppose not x in ( dom f);

          hence (f . x) is rational by FUNCT_1:def 2;

        end;

      end;

      assume

       A2: for x holds (f . x) is rational;

      let y be object;

      assume y in ( rng f);

      then

      consider x be object such that x in ( dom f) and

       A3: (f . x) = y by FUNCT_1:def 3;

      (f . x) is rational by A2;

      hence thesis by A3, RAT_1:def 2;

    end;

    theorem :: VALUED_0:11

    

     Th11: f is INT -valued iff for x holds (f . x) is integer

    proof

      hereby

        assume

         A1: f is INT -valued;

        let x;

        per cases ;

          suppose x in ( dom f);

          then (f . x) in ( rng f) by FUNCT_1:def 3;

          hence (f . x) is integer by A1;

        end;

          suppose not x in ( dom f);

          hence (f . x) is integer by FUNCT_1:def 2;

        end;

      end;

      assume

       A2: for x holds (f . x) is integer;

      let y be object;

      assume y in ( rng f);

      then

      consider x be object such that x in ( dom f) and

       A3: (f . x) = y by FUNCT_1:def 3;

      (f . x) is integer by A2;

      hence thesis by A3, INT_1:def 2;

    end;

    theorem :: VALUED_0:12

    

     Th12: f is natural-valued iff for x holds (f . x) is natural

    proof

      hereby

        assume

         A1: f is natural-valued;

        let x;

        per cases ;

          suppose x in ( dom f);

          hence (f . x) is natural by A1;

        end;

          suppose not x in ( dom f);

          hence (f . x) is natural by FUNCT_1:def 2;

        end;

      end;

      assume for x holds (f . x) is natural;

      then for x st x in ( dom f) holds (f . x) is natural;

      hence thesis;

    end;

    registration

      let f be complex-valued Function;

      let x be object;

      cluster (f . x) -> complex;

      coherence by Th7;

    end

    registration

      let f be ext-real-valued Function;

      let x be object;

      cluster (f . x) -> ext-real;

      coherence by Th8;

    end

    registration

      let f be real-valued Function;

      let x be object;

      cluster (f . x) -> real;

      coherence by Th9;

    end

    registration

      let f be RAT -valued Function;

      let x be object;

      cluster (f . x) -> rational;

      coherence by Th10;

    end

    registration

      let f be INT -valued Function;

      let x be object;

      cluster (f . x) -> integer;

      coherence by Th11;

    end

    registration

      let f be natural-valued Function;

      let x be object;

      cluster (f . x) -> natural;

      coherence by Th12;

    end

    registration

      let X;

      let x be Complex;

      cluster (X --> x) -> complex-valued;

      coherence

      proof

        ( rng (X --> x)) c= COMPLEX by MEMBERED: 1;

        hence thesis;

      end;

    end

    registration

      let X;

      let x be ExtReal;

      cluster (X --> x) -> ext-real-valued;

      coherence

      proof

        ( rng (X --> x)) c= ExtREAL by MEMBERED: 2;

        hence thesis;

      end;

    end

    registration

      let X;

      let x be Real;

      cluster (X --> x) -> real-valued;

      coherence

      proof

        ( rng (X --> x)) c= REAL by MEMBERED: 3;

        hence thesis;

      end;

    end

    registration

      let X;

      let x be Rational;

      cluster (X --> x) -> RAT -valued;

      coherence

      proof

        ( rng (X --> x)) c= RAT by MEMBERED: 4;

        hence thesis;

      end;

    end

    registration

      let X;

      let x be Integer;

      cluster (X --> x) -> INT -valued;

      coherence

      proof

        ( rng (X --> x)) c= INT by MEMBERED: 5;

        hence thesis;

      end;

    end

    registration

      let X;

      let x be Nat;

      cluster (X --> x) -> natural-valued;

      coherence

      proof

        ( rng (X --> x)) c= NAT by MEMBERED: 6;

        hence thesis;

      end;

    end

    registration

      let f,g be complex-valued Function;

      cluster (f +* g) -> complex-valued;

      coherence

      proof

        ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

        then ( rng (f +* g)) c= COMPLEX by MEMBERED: 1;

        hence thesis;

      end;

    end

    registration

      let f,g be ext-real-valued Function;

      cluster (f +* g) -> ext-real-valued;

      coherence

      proof

        ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

        then ( rng (f +* g)) c= ExtREAL by MEMBERED: 2;

        hence thesis;

      end;

    end

    registration

      let f,g be real-valued Function;

      cluster (f +* g) -> real-valued;

      coherence

      proof

        ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

        then ( rng (f +* g)) c= REAL by MEMBERED: 3;

        hence thesis;

      end;

    end

    registration

      let f,g be RAT -valued Function;

      cluster (f +* g) -> RAT -valued;

      coherence

      proof

        ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

        then ( rng (f +* g)) c= RAT by MEMBERED: 4;

        hence thesis;

      end;

    end

    registration

      let f,g be INT -valued Function;

      cluster (f +* g) -> INT -valued;

      coherence

      proof

        ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

        then ( rng (f +* g)) c= INT by MEMBERED: 5;

        hence thesis;

      end;

    end

    registration

      let f,g be natural-valued Function;

      cluster (f +* g) -> natural-valued;

      coherence

      proof

        ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

        then ( rng (f +* g)) c= NAT by MEMBERED: 6;

        hence thesis;

      end;

    end

    registration

      let x;

      let y be Complex;

      cluster (x .--> y) -> complex-valued;

      coherence ;

    end

    registration

      let x;

      let y be ExtReal;

      cluster (x .--> y) -> ext-real-valued;

      coherence ;

    end

    registration

      let x;

      let y be Real;

      cluster (x .--> y) -> real-valued;

      coherence ;

    end

    registration

      let x;

      let y be Rational;

      cluster (x .--> y) -> RAT -valued;

      coherence ;

    end

    registration

      let x;

      let y be Integer;

      cluster (x .--> y) -> INT -valued;

      coherence ;

    end

    registration

      let x;

      let y be Nat;

      cluster (x .--> y) -> natural-valued;

      coherence ;

    end

    registration

      let X;

      let Y be complex-membered set;

      cluster -> complex-valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( rng R) c= COMPLEX by MEMBERED: 1;

      end;

    end

    registration

      let X;

      let Y be ext-real-membered set;

      cluster -> ext-real-valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( rng R) c= ExtREAL by MEMBERED: 2;

      end;

    end

    registration

      let X;

      let Y be real-membered set;

      cluster -> real-valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( rng R) c= REAL by MEMBERED: 3;

      end;

    end

    registration

      let X;

      let Y be rational-membered set;

      cluster -> RAT -valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( rng R) c= RAT by MEMBERED: 4;

      end;

    end

    registration

      let X;

      let Y be integer-membered set;

      cluster -> INT -valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( rng R) c= INT by MEMBERED: 5;

      end;

    end

    registration

      let X;

      let Y be natural-membered set;

      cluster -> natural-valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( rng R) c= NAT by MEMBERED: 6;

      end;

    end

    registration

      let X;

      let Y be complex-membered set;

      cluster [:X, Y:] -> complex-valued;

      coherence

      proof

        ( rng [:X, Y:]) c= Y by RELAT_1: 159;

        hence ( rng [:X, Y:]) c= COMPLEX by MEMBERED: 1;

      end;

    end

    registration

      let X;

      let Y be ext-real-membered set;

      cluster [:X, Y:] -> ext-real-valued;

      coherence

      proof

        ( rng [:X, Y:]) c= Y by RELAT_1: 159;

        hence ( rng [:X, Y:]) c= ExtREAL by MEMBERED: 2;

      end;

    end

    registration

      let X;

      let Y be real-membered set;

      cluster [:X, Y:] -> real-valued;

      coherence

      proof

        ( rng [:X, Y:]) c= Y by RELAT_1: 159;

        hence ( rng [:X, Y:]) c= REAL by MEMBERED: 3;

      end;

    end

    registration

      let X;

      let Y be rational-membered set;

      cluster [:X, Y:] -> RAT -valued;

      coherence

      proof

        ( rng [:X, Y:]) c= Y by RELAT_1: 159;

        hence ( rng [:X, Y:]) c= RAT by MEMBERED: 4;

      end;

    end

    registration

      let X;

      let Y be integer-membered set;

      cluster [:X, Y:] -> INT -valued;

      coherence

      proof

        ( rng [:X, Y:]) c= Y by RELAT_1: 159;

        hence ( rng [:X, Y:]) c= INT by MEMBERED: 5;

      end;

    end

    registration

      let X;

      let Y be natural-membered set;

      cluster [:X, Y:] -> natural-valued;

      coherence

      proof

        ( rng [:X, Y:]) c= Y by RELAT_1: 159;

        hence ( rng [:X, Y:]) c= NAT by MEMBERED: 6;

      end;

    end

    registration

      cluster non empty constant natural-valued INT -valued RAT -valued for Function;

      existence

      proof

        take (1 .--> 1);

        thus thesis;

      end;

    end

    theorem :: VALUED_0:13

    for f be non empty constant complex-valued Function holds ex r be Complex st for x be object st x in ( dom f) holds (f . x) = r

    proof

      let f be non empty constant complex-valued Function;

      consider r be object such that

       A1: for x be object st x in ( dom f) holds (f . x) = r by FUNCOP_1: 78;

      consider x be object such that

       A2: x in ( dom f) by XBOOLE_0:def 1;

      r = (f . x) by A1, A2;

      hence thesis by A1;

    end;

    theorem :: VALUED_0:14

    for f be non empty constant ext-real-valued Function holds ex r be ExtReal st for x be object st x in ( dom f) holds (f . x) = r

    proof

      let f be non empty constant ext-real-valued Function;

      consider r be object such that

       A1: for x be object st x in ( dom f) holds (f . x) = r by FUNCOP_1: 78;

      consider x be object such that

       A2: x in ( dom f) by XBOOLE_0:def 1;

      r = (f . x) by A1, A2;

      hence thesis by A1;

    end;

    theorem :: VALUED_0:15

    for f be non empty constant real-valued Function holds ex r be Real st for x be object st x in ( dom f) holds (f . x) = r

    proof

      let f be non empty constant real-valued Function;

      consider r be object such that

       A1: for x be object st x in ( dom f) holds (f . x) = r by FUNCOP_1: 78;

      consider x be object such that

       A2: x in ( dom f) by XBOOLE_0:def 1;

      r = (f . x) by A1, A2;

      hence thesis by A1;

    end;

    theorem :: VALUED_0:16

    for f be non empty constant RAT -valued Function holds ex r be Rational st for x be object st x in ( dom f) holds (f . x) = r

    proof

      let f be non empty constant RAT -valued Function;

      consider r be object such that

       A1: for x be object st x in ( dom f) holds (f . x) = r by FUNCOP_1: 78;

      consider x be object such that

       A2: x in ( dom f) by XBOOLE_0:def 1;

      r = (f . x) by A1, A2;

      hence thesis by A1;

    end;

    theorem :: VALUED_0:17

    for f be non empty constant INT -valued Function holds ex r be Integer st for x be object st x in ( dom f) holds (f . x) = r

    proof

      let f be non empty constant INT -valued Function;

      consider r be object such that

       A1: for x be object st x in ( dom f) holds (f . x) = r by FUNCOP_1: 78;

      consider x be object such that

       A2: x in ( dom f) by XBOOLE_0:def 1;

      r = (f . x) by A1, A2;

      hence thesis by A1;

    end;

    theorem :: VALUED_0:18

    for f be non empty constant natural-valued Function holds ex r be Nat st for x be object st x in ( dom f) holds (f . x) = r

    proof

      let f be non empty constant natural-valued Function;

      consider r be object such that

       A1: for x be object st x in ( dom f) holds (f . x) = r by FUNCOP_1: 78;

      consider x be object such that

       A2: x in ( dom f) by XBOOLE_0:def 1;

      r = (f . x) by A1, A2;

      hence thesis by A1;

    end;

    begin

    reserve e1,e2 for ExtReal;

    definition

      let f be ext-real-valued Function;

      :: VALUED_0:def13

      attr f is increasing means

      : Def9: for e1, e2 st e1 in ( dom f) & e2 in ( dom f) & e1 < e2 holds (f . e1) < (f . e2);

      :: VALUED_0:def14

      attr f is decreasing means

      : Def10: for e1, e2 st e1 in ( dom f) & e2 in ( dom f) & e1 < e2 holds (f . e1) > (f . e2);

      :: VALUED_0:def15

      attr f is non-decreasing means

      : Def11: for e1, e2 st e1 in ( dom f) & e2 in ( dom f) & e1 <= e2 holds (f . e1) <= (f . e2);

      :: VALUED_0:def16

      attr f is non-increasing means

      : Def12: for e1, e2 st e1 in ( dom f) & e2 in ( dom f) & e1 <= e2 holds (f . e1) >= (f . e2);

    end

    registration

      cluster trivial -> increasing decreasing for ext-real-valued Function;

      coherence by ZFMISC_1:def 10;

    end

    registration

      cluster increasing -> non-decreasing for ext-real-valued Function;

      coherence

      proof

        let f be ext-real-valued Function;

        assume

         A1: f is increasing;

        let e1, e2 such that

         A2: e1 in ( dom f) & e2 in ( dom f) and

         A3: e1 <= e2;

        per cases by A3, XXREAL_0: 1;

          suppose e1 = e2;

          hence thesis;

        end;

          suppose e1 < e2;

          hence thesis by A1, A2;

        end;

      end;

      cluster decreasing -> non-increasing for ext-real-valued Function;

      coherence

      proof

        let f be ext-real-valued Function;

        assume

         A4: f is decreasing;

        let e1, e2 such that

         A5: e1 in ( dom f) & e2 in ( dom f) and

         A6: e1 <= e2;

        per cases by A6, XXREAL_0: 1;

          suppose e1 = e2;

          hence thesis;

        end;

          suppose e1 < e2;

          hence thesis by A4, A5;

        end;

      end;

    end

    registration

      let f,g be increasing ext-real-valued Function;

      cluster (g * f) -> increasing;

      coherence

      proof

        let e1, e2;

        assume that

         A1: e1 in ( dom (g * f)) and

         A2: e2 in ( dom (g * f));

        

         A3: e1 in ( dom f) by A1, FUNCT_1: 11;

        then

         A4: ((g * f) . e1) = (g . (f . e1)) by FUNCT_1: 13;

        

         A5: e2 in ( dom f) by A2, FUNCT_1: 11;

        then

         A6: ((g * f) . e2) = (g . (f . e2)) by FUNCT_1: 13;

        assume e1 < e2;

        then

         A7: (f . e1) < (f . e2) by A3, A5, Def9;

        (f . e1) in ( dom g) & (f . e2) in ( dom g) by A1, A2, FUNCT_1: 11;

        hence thesis by A4, A6, A7, Def9;

      end;

    end

    registration

      let f,g be non-decreasing ext-real-valued Function;

      cluster (g * f) -> non-decreasing;

      coherence

      proof

        let e1, e2;

        assume that

         A1: e1 in ( dom (g * f)) and

         A2: e2 in ( dom (g * f));

        

         A3: e1 in ( dom f) by A1, FUNCT_1: 11;

        then

         A4: ((g * f) . e1) = (g . (f . e1)) by FUNCT_1: 13;

        

         A5: e2 in ( dom f) by A2, FUNCT_1: 11;

        then

         A6: ((g * f) . e2) = (g . (f . e2)) by FUNCT_1: 13;

        assume e1 <= e2;

        then

         A7: (f . e1) <= (f . e2) by A3, A5, Def11;

        (f . e1) in ( dom g) & (f . e2) in ( dom g) by A1, A2, FUNCT_1: 11;

        hence thesis by A4, A6, A7, Def11;

      end;

    end

    registration

      let f,g be decreasing ext-real-valued Function;

      cluster (g * f) -> increasing;

      coherence

      proof

        let e1, e2;

        assume that

         A1: e1 in ( dom (g * f)) and

         A2: e2 in ( dom (g * f));

        

         A3: e1 in ( dom f) by A1, FUNCT_1: 11;

        then

         A4: ((g * f) . e1) = (g . (f . e1)) by FUNCT_1: 13;

        

         A5: e2 in ( dom f) by A2, FUNCT_1: 11;

        then

         A6: ((g * f) . e2) = (g . (f . e2)) by FUNCT_1: 13;

        assume e1 < e2;

        then

         A7: (f . e1) > (f . e2) by A3, A5, Def10;

        (f . e1) in ( dom g) & (f . e2) in ( dom g) by A1, A2, FUNCT_1: 11;

        hence thesis by A4, A6, A7, Def10;

      end;

    end

    registration

      let f,g be non-increasing ext-real-valued Function;

      cluster (g * f) -> non-decreasing;

      coherence

      proof

        let e1, e2;

        assume that

         A1: e1 in ( dom (g * f)) and

         A2: e2 in ( dom (g * f));

        

         A3: e1 in ( dom f) by A1, FUNCT_1: 11;

        then

         A4: ((g * f) . e1) = (g . (f . e1)) by FUNCT_1: 13;

        

         A5: e2 in ( dom f) by A2, FUNCT_1: 11;

        then

         A6: ((g * f) . e2) = (g . (f . e2)) by FUNCT_1: 13;

        assume e1 <= e2;

        then

         A7: (f . e1) >= (f . e2) by A3, A5, Def12;

        (f . e1) in ( dom g) & (f . e2) in ( dom g) by A1, A2, FUNCT_1: 11;

        hence thesis by A4, A6, A7, Def12;

      end;

    end

    registration

      let f be decreasing ext-real-valued Function;

      let g be increasing ext-real-valued Function;

      cluster (g * f) -> decreasing;

      coherence

      proof

        let e1, e2;

        assume that

         A1: e1 in ( dom (g * f)) and

         A2: e2 in ( dom (g * f));

        

         A3: e1 in ( dom f) by A1, FUNCT_1: 11;

        then

         A4: ((g * f) . e1) = (g . (f . e1)) by FUNCT_1: 13;

        

         A5: e2 in ( dom f) by A2, FUNCT_1: 11;

        then

         A6: ((g * f) . e2) = (g . (f . e2)) by FUNCT_1: 13;

        assume e1 < e2;

        then

         A7: (f . e1) > (f . e2) by A3, A5, Def10;

        (f . e1) in ( dom g) & (f . e2) in ( dom g) by A1, A2, FUNCT_1: 11;

        hence thesis by A4, A6, A7, Def9;

      end;

      cluster (f * g) -> decreasing;

      coherence

      proof

        let e1, e2;

        assume that

         A8: e1 in ( dom (f * g)) and

         A9: e2 in ( dom (f * g));

        

         A10: e1 in ( dom g) by A8, FUNCT_1: 11;

        then

         A11: ((f * g) . e1) = (f . (g . e1)) by FUNCT_1: 13;

        

         A12: e2 in ( dom g) by A9, FUNCT_1: 11;

        then

         A13: ((f * g) . e2) = (f . (g . e2)) by FUNCT_1: 13;

        assume e1 < e2;

        then

         A14: (g . e1) < (g . e2) by A10, A12, Def9;

        (g . e1) in ( dom f) & (g . e2) in ( dom f) by A8, A9, FUNCT_1: 11;

        hence thesis by A11, A13, A14, Def10;

      end;

    end

    registration

      let f be non-increasing ext-real-valued Function;

      let g be non-decreasing ext-real-valued Function;

      cluster (g * f) -> non-increasing;

      coherence

      proof

        let e1, e2;

        assume that

         A1: e1 in ( dom (g * f)) and

         A2: e2 in ( dom (g * f));

        

         A3: e1 in ( dom f) by A1, FUNCT_1: 11;

        then

         A4: ((g * f) . e1) = (g . (f . e1)) by FUNCT_1: 13;

        

         A5: e2 in ( dom f) by A2, FUNCT_1: 11;

        then

         A6: ((g * f) . e2) = (g . (f . e2)) by FUNCT_1: 13;

        assume e1 <= e2;

        then

         A7: (f . e1) >= (f . e2) by A3, A5, Def12;

        (f . e1) in ( dom g) & (f . e2) in ( dom g) by A1, A2, FUNCT_1: 11;

        hence thesis by A4, A6, A7, Def11;

      end;

      cluster (f * g) -> non-increasing;

      coherence

      proof

        let e1, e2;

        assume that

         A8: e1 in ( dom (f * g)) and

         A9: e2 in ( dom (f * g));

        

         A10: e1 in ( dom g) by A8, FUNCT_1: 11;

        then

         A11: ((f * g) . e1) = (f . (g . e1)) by FUNCT_1: 13;

        

         A12: e2 in ( dom g) by A9, FUNCT_1: 11;

        then

         A13: ((f * g) . e2) = (f . (g . e2)) by FUNCT_1: 13;

        assume e1 <= e2;

        then

         A14: (g . e1) <= (g . e2) by A10, A12, Def11;

        (g . e1) in ( dom f) & (g . e2) in ( dom f) by A8, A9, FUNCT_1: 11;

        hence thesis by A11, A13, A14, Def12;

      end;

    end

    registration

      let X be ext-real-membered set;

      cluster ( id X) -> increasing;

      coherence

      proof

        ( id X) is increasing

        proof

          let e1, e2;

          assume that

           A1: e1 in ( dom ( id X)) and

           A2: e2 in ( dom ( id X));

          (( id X) . e1) = e1 by A1, FUNCT_1: 18;

          hence thesis by A2, FUNCT_1: 18;

        end;

        hence thesis;

      end;

    end

    registration

      cluster increasing for sequence of NAT ;

      existence

      proof

        take ( id NAT );

        thus thesis;

      end;

    end

    definition

      let s be ManySortedSet of NAT ;

      :: VALUED_0:def17

      mode subsequence of s -> ManySortedSet of NAT means

      : Def13: ex N be increasing sequence of NAT st it = (s * N);

      existence

      proof

        take s, ( id NAT );

        ( dom s) = NAT by PARTFUN1:def 2;

        hence thesis by RELAT_1: 52;

      end;

    end

    

     Lm1: for x be non empty set, M be ManySortedSet of NAT , s be subsequence of M holds ( rng s) c= ( rng M)

    proof

      let x be non empty set, M be ManySortedSet of NAT , s be subsequence of M;

      ex N be increasing sequence of NAT st s = (M * N) by Def13;

      hence ( rng s) c= ( rng M) by RELAT_1: 26;

    end;

    registration

      let X be non empty set, s be X -valued ManySortedSet of NAT ;

      cluster -> X -valued for subsequence of s;

      coherence

      proof

        let ss be subsequence of s;

        ( rng ss) c= ( rng s) by Lm1;

        hence ( rng ss) c= X by XBOOLE_1: 1;

      end;

    end

    definition

      let X be non empty set, s be sequence of X;

      :: original: subsequence

      redefine

      mode subsequence of s -> sequence of X ;

      coherence

      proof

        let ss be subsequence of s;

        ( rng ss) c= X & ( dom ss) = NAT by PARTFUN1:def 2;

        hence ss is sequence of X by RELSET_1: 4;

      end;

    end

    definition

      let X be non empty set, s be sequence of X, k be Nat;

      :: original: ^\

      redefine

      func s ^\ k -> subsequence of s ;

      coherence

      proof

        set N = (( id NAT ) ^\ k);

        N is increasing

        proof

          let e1, e2;

          assume e1 in ( dom N) & e2 in ( dom N);

          then

          reconsider i = e1, j = e2 as Element of NAT ;

          reconsider jk = (j + k), ik = (i + k) as Element of NAT by ORDINAL1:def 12;

          

           A1: (N . j) = (( id NAT ) . jk) by NAT_1:def 3

          .= jk;

          assume

           A2: e1 < e2;

          (N . i) = (( id NAT ) . ik) by NAT_1:def 3

          .= ik;

          hence thesis by A1, A2, XREAL_1: 6;

        end;

        then

        reconsider N as increasing sequence of NAT ;

        thus (s ^\ k) is subsequence of s

        proof

          take N;

          

          thus (s ^\ k) = ((s * ( id NAT )) ^\ k) by FUNCT_2: 17

          .= (s * N) by NAT_1: 50;

        end;

      end;

    end

    reserve s,s1,s2,s3 for sequence of X;

    reserve XX for non empty set,

ss,ss1,ss2,ss3 for sequence of XX;

    theorem :: VALUED_0:19

    ss is subsequence of ss

    proof

      take ( id NAT );

      thus thesis by FUNCT_2: 17;

    end;

    theorem :: VALUED_0:20

    ss1 is subsequence of ss2 & ss2 is subsequence of ss3 implies ss1 is subsequence of ss3

    proof

      given N1 be increasing sequence of NAT such that

       A1: ss1 = (ss2 * N1);

      given N2 be increasing sequence of NAT such that

       A2: ss2 = (ss3 * N2);

      take (N2 * N1);

      thus thesis by A1, A2, RELAT_1: 36;

    end;

    registration

      let X;

      cluster constant for sequence of X;

      existence

      proof

        per cases ;

          suppose X = {} ;

          then

          reconsider s = {} as sequence of X by FUNCT_2:def 1, RELSET_1: 12;

          take s;

          thus thesis;

        end;

          suppose X <> {} ;

          then

          consider x be object such that

           A1: x in X by XBOOLE_0:def 1;

          reconsider s = ( NAT --> x) as sequence of X by A1, FUNCOP_1: 45;

          take s;

          thus thesis;

        end;

      end;

    end

    theorem :: VALUED_0:21

    

     Th21: for ss1 be subsequence of ss holds ( rng ss1) c= ( rng ss)

    proof

      let ss1 be subsequence of ss;

      let x be object;

      consider N be increasing sequence of NAT such that

       A1: ss1 = (ss * N) by Def13;

      assume x in ( rng ss1);

      then

      consider n be object such that

       A2: n in NAT and

       A3: x = (ss1 . n) by FUNCT_2: 11;

      

       A4: (N . n) in NAT by A2, FUNCT_2: 5;

      x = (ss . (N . n)) by A1, A2, A3, FUNCT_2: 15;

      hence thesis by A4, FUNCT_2: 4;

    end;

    registration

      let X be non empty set;

      let s be constant sequence of X;

      cluster -> constant for subsequence of s;

      coherence

      proof

        let s1 be subsequence of s;

        ( rng s1) c= ( rng s) by Th21;

        hence thesis;

      end;

    end

    definition

      let X be non empty set, N be increasing sequence of NAT , s be sequence of X;

      :: original: *

      redefine

      func s * N -> subsequence of s ;

      correctness by Def13;

    end

    reserve X,Y for non empty set,

Z for set;

    reserve s,s1 for sequence of X,

h,h1 for PartFunc of X, Y,

h2 for PartFunc of Y, Z,

x for Element of X,

N for increasing sequence of NAT ;

    theorem :: VALUED_0:22

    ( rng s) c= ( dom h) & s1 is subsequence of s implies (h /* s1) is subsequence of (h /* s)

    proof

      assume that

       A1: ( rng s) c= ( dom h) and

       A2: s1 is subsequence of s;

      consider N such that

       A3: s1 = (s * N) by A2, Def13;

      take N;

      thus thesis by A1, A3, FUNCT_2: 110;

    end;

    registration

      let X be with_non-empty_element set;

      cluster non-empty for sequence of X;

      existence

      proof

        consider x be non empty set such that

         A1: x in X by SETFAM_1:def 10;

        reconsider s = ( NAT --> x) as sequence of X by A1, FUNCOP_1: 45;

        take s;

        thus thesis;

      end;

    end

    registration

      let X be with_non-empty_element set, s be non-empty sequence of X;

      cluster -> non-empty for subsequence of s;

      coherence

      proof

        let s1 be subsequence of s;

        ( rng s1) c= ( rng s) by Th21;

        hence not {} in ( rng s1);

      end;

    end

    reserve i,j for Nat;

    definition

      let X be non empty set, s be sequence of X;

      :: original: constant

      redefine

      :: VALUED_0:def18

      attr s is constant means ex x be Element of X st for n be Nat holds (s . n) = x;

      compatibility

      proof

        hereby

          assume s is constant;

          then

          consider x be Element of X such that

           A1: for n be Element of NAT st n in ( dom s) holds (s . n) = x;

          take x;

          let n be Nat;

          ( dom s) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12;

          hence (s . n) = x by A1;

        end;

        given x be Element of X such that

         A2: for n be Nat holds (s . n) = x;

        take x;

        thus thesis by A2;

      end;

    end

    theorem :: VALUED_0:23

    

     Th23: for X be set holds for s be constant sequence of X holds (s . i) = (s . j)

    proof

      let X be set;

      let s be constant sequence of X;

      per cases ;

        suppose

         A1: X is empty;

        then (s . i) = {} ;

        hence thesis by A1;

      end;

        suppose not X is empty;

        then ( dom s) = NAT by FUNCT_2:def 1;

        then i in ( dom s) & j in ( dom s) by ORDINAL1:def 12;

        hence thesis by FUNCT_1:def 10;

      end;

    end;

    theorem :: VALUED_0:24

    (for i, j holds (s . i) = (s . j)) implies s is constant;

    theorem :: VALUED_0:25

    (for i holds (s . i) = (s . (i + 1))) implies s is constant

    proof

      assume

       A1: for i holds (s . i) = (s . (i + 1));

      now

        let i, j;

         A2:

        now

          let i, j such that

           A3: i <= j;

          defpred P[ Nat] means i <= $1 implies (s . i) = (s . $1);

          

           A4: for j be Nat st P[j] holds P[(j + 1)]

          proof

            let j be Nat such that

             A5: P[j];

            assume i <= (j + 1);

            then i < (j + 1) or i = (j + 1) by XXREAL_0: 1;

            hence thesis by A1, A5, NAT_1: 13;

          end;

          

           A6: P[ 0 ] by NAT_1: 3;

          for j be Nat holds P[j] from NAT_1:sch 2( A6, A4);

          hence (s . i) = (s . j) by A3;

        end;

        i <= j or j <= i;

        hence (s . i) = (s . j) by A2;

      end;

      hence thesis;

    end;

    theorem :: VALUED_0:26

    s is constant & s1 is subsequence of s implies s = s1

    proof

      assume that

       A1: s is constant and

       A2: s1 is subsequence of s;

      let n be Element of NAT ;

      consider N such that

       A3: s1 = (s * N) by A2, Def13;

      

      thus (s1 . n) = (s . (N . n)) by A3, FUNCT_2: 15

      .= (s . n) by A1, Th23;

    end;

    reserve n for Nat;

    theorem :: VALUED_0:27

    

     Th27: ( rng s) c= ( dom h) implies ((h /* s) ^\ n) = (h /* (s ^\ n))

    proof

      assume

       A1: ( rng s) c= ( dom h);

      let m be Element of NAT ;

      

       A2: ( rng (s ^\ n)) c= ( rng s) by Th21;

      reconsider mn = (m + n) as Element of NAT by ORDINAL1:def 12;

      

      thus (((h /* s) ^\ n) . m) = ((h /* s) . (m + n)) by NAT_1:def 3

      .= (h . (s . mn)) by A1, FUNCT_2: 108

      .= (h . ((s ^\ n) . m)) by NAT_1:def 3

      .= ((h /* (s ^\ n)) . m) by A1, A2, FUNCT_2: 108, XBOOLE_1: 1;

    end;

    theorem :: VALUED_0:28

    

     Th28: (s . n) in ( rng s)

    proof

      n in NAT by ORDINAL1:def 12;

      hence thesis by FUNCT_2: 112;

    end;

    theorem :: VALUED_0:29

    h is total implies (h /* (s ^\ n)) = ((h /* s) ^\ n)

    proof

      assume h is total;

      then ( dom h) = X by PARTFUN1:def 2;

      then ( rng s) c= ( dom h);

      hence thesis by Th27;

    end;

    theorem :: VALUED_0:30

    

     Th30: ( rng s) c= ( dom h) implies (h .: ( rng s)) = ( rng (h /* s))

    proof

      assume

       A1: ( rng s) c= ( dom h);

      now

        let r be Element of Y;

        thus r in (h .: ( rng s)) implies r in ( rng (h /* s))

        proof

          assume r in (h .: ( rng s));

          then

          consider p be Element of X such that p in ( dom h) and

           A2: p in ( rng s) and

           A3: r = (h . p) by PARTFUN2: 59;

          consider n be Element of NAT such that

           A4: p = (s . n) by A2, FUNCT_2: 113;

          r = ((h /* s) . n) by A1, A3, A4, FUNCT_2: 108;

          hence thesis by Th28;

        end;

        assume r in ( rng (h /* s));

        then

        consider n be Element of NAT such that

         A5: ((h /* s) . n) = r by FUNCT_2: 113;

        

         A6: (s . n) in ( rng s) by Th28;

        r = (h . (s . n)) by A1, A5, FUNCT_2: 108;

        hence r in (h .: ( rng s)) by A1, A6, FUNCT_1:def 6;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: VALUED_0:31

    ( rng s) c= ( dom (h2 * h1)) implies (h2 /* (h1 /* s)) = ((h2 * h1) /* s)

    proof

      assume

       A1: ( rng s) c= ( dom (h2 * h1));

      now

        let n be Element of NAT ;

        

         A2: ( rng s) c= ( dom h1) by A1, FUNCT_1: 101;

        (h1 .: ( rng s)) c= ( dom h2) by A1, FUNCT_1: 101;

        then

         A3: ( rng (h1 /* s)) c= ( dom h2) by A2, Th30;

        (s . n) in ( rng s) by Th28;

        then

         A4: (s . n) in ( dom h1) by A1, FUNCT_1: 11;

        

        thus (((h2 * h1) /* s) . n) = ((h2 * h1) . (s . n)) by A1, FUNCT_2: 108

        .= (h2 . (h1 . (s . n))) by A4, FUNCT_1: 13

        .= (h2 . ((h1 /* s) . n)) by A2, FUNCT_2: 108

        .= ((h2 /* (h1 /* s)) . n) by A3, FUNCT_2: 108;

      end;

      hence thesis;

    end;

    definition

      let f be ext-real-valued Function;

      :: VALUED_0:def19

      attr f is zeroed means (f . {} ) = 0 ;

    end

    registration

      cluster COMPLEX -valued -> complex-valued for Relation;

      coherence ;

      cluster ExtREAL -valued -> ext-real-valued for Relation;

      coherence ;

      cluster REAL -valued -> real-valued for Relation;

      coherence ;

      cluster NAT -valued -> natural-valued for Relation;

      coherence ;

    end

    definition

      let s be ManySortedSet of NAT ;

      :: original: constant

      redefine

      :: VALUED_0:def20

      attr s is constant means ex x be set st for n be Nat holds (s . n) = x;

      compatibility

      proof

        

         A1: ( dom s) = NAT by PARTFUN1:def 2;

        hereby

          assume

           A2: s is constant;

          take x = (s . 0 );

          let n be Nat;

           0 in ( dom s) & n in ( dom s) by A1, ORDINAL1:def 12;

          hence (s . n) = x by A2;

        end;

        given x be set such that

         A3: for n be Nat holds (s . n) = x;

        let n1,n2 be object;

        assume

         A4: n1 in ( dom s) & n2 in ( dom s);

        

        hence (s . n1) = x by A3

        .= (s . n2) by A3, A4;

      end;

    end

    theorem :: VALUED_0:32

    for x be non empty set, M be ManySortedSet of NAT , s be subsequence of M holds ( rng s) c= ( rng M) by Lm1;

    registration

      let X be set;

      cluster natural-valued for ManySortedSet of X;

      existence

      proof

        take (X --> 0 );

        thus thesis;

      end;

    end