valued_2.miz



    begin

    reserve x,y for object,

X,X1,X2 for set;

     Lm1:

    now

      let X1,X2,X3 be set;

      

      thus (X1 /\ (X2 /\ X3)) = (((X1 /\ X1) /\ X2) /\ X3) by XBOOLE_1: 16

      .= ((X1 /\ (X1 /\ X2)) /\ X3) by XBOOLE_1: 16

      .= ((X1 /\ X2) /\ (X1 /\ X3)) by XBOOLE_1: 16;

    end;

    definition

      let Y be functional set;

      :: VALUED_2:def1

      func DOMS (Y) -> set equals ( union the set of all ( dom f) where f be Element of Y);

      coherence ;

    end

    definition

      let X;

      :: VALUED_2:def2

      attr X is complex-functions-membered means

      : Def2: x in X implies x is complex-valued Function;

    end

    definition

      let X;

      :: VALUED_2:def3

      attr X is ext-real-functions-membered means

      : Def3: x in X implies x is ext-real-valued Function;

    end

    definition

      let X;

      :: VALUED_2:def4

      attr X is real-functions-membered means

      : Def4: x in X implies x is real-valued Function;

    end

    definition

      let X;

      :: VALUED_2:def5

      attr X is rational-functions-membered means

      : Def5: x in X implies x is RAT -valued Function;

    end

    definition

      let X;

      :: VALUED_2:def6

      attr X is integer-functions-membered means

      : Def6: x in X implies x is INT -valued Function;

    end

    definition

      let X;

      :: VALUED_2:def7

      attr X is natural-functions-membered means

      : Def7: x in X implies x is natural-valued Function;

    end

    registration

      cluster natural-functions-membered -> integer-functions-membered for set;

      coherence

      proof

        let X;

        assume

         A1: for x be object st x in X holds x is natural-valued Function;

        let x;

        assume x in X;

        then x is natural-valued Function by A1;

        hence thesis;

      end;

      cluster integer-functions-membered -> rational-functions-membered for set;

      coherence

      proof

        let X;

        assume

         A2: for x be object st x in X holds x is INT -valued Function;

        let x;

        assume x in X;

        then x is INT -valued Function by A2;

        hence thesis;

      end;

      cluster rational-functions-membered -> real-functions-membered for set;

      coherence ;

      cluster real-functions-membered -> complex-functions-membered for set;

      coherence ;

      cluster real-functions-membered -> ext-real-functions-membered for set;

      coherence ;

    end

    registration

      cluster empty -> natural-functions-membered for set;

      coherence ;

    end

    registration

      let f be complex-valued Function;

      cluster {f} -> complex-functions-membered;

      coherence by TARSKI:def 1;

    end

    registration

      cluster complex-functions-membered -> functional for set;

      coherence

      proof

        let X;

        assume

         A1: X is complex-functions-membered;

        let x;

        thus thesis by A1;

      end;

      cluster ext-real-functions-membered -> functional for set;

      coherence

      proof

        let X;

        assume

         A2: X is ext-real-functions-membered;

        let x;

        thus thesis by A2;

      end;

    end

    set ff = the natural-valued Function;

    registration

      cluster natural-functions-membered non empty for set;

      existence

      proof

        take {ff};

        thus for x be object st x in {ff} holds x is natural-valued Function by TARSKI:def 1;

        thus thesis;

      end;

    end

    registration

      let X be complex-functions-membered set;

      cluster -> complex-functions-membered for Subset of X;

      coherence by Def2;

    end

    registration

      let X be ext-real-functions-membered set;

      cluster -> ext-real-functions-membered for Subset of X;

      coherence by Def3;

    end

    registration

      let X be real-functions-membered set;

      cluster -> real-functions-membered for Subset of X;

      coherence by Def4;

    end

    registration

      let X be rational-functions-membered set;

      cluster -> rational-functions-membered for Subset of X;

      coherence by Def5;

    end

    registration

      let X be integer-functions-membered set;

      cluster -> integer-functions-membered for Subset of X;

      coherence by Def6;

    end

    registration

      let X be natural-functions-membered set;

      cluster -> natural-functions-membered for Subset of X;

      coherence by Def7;

    end

    definition

      set A = COMPLEX ;

      let D be set;

      defpred P[ object] means $1 is PartFunc of D, A;

      :: VALUED_2:def8

      func C_PFuncs (D) -> set means

      : Def8: for f be object holds f in it iff f is PartFunc of D, COMPLEX ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is PartFunc of D, A by A1;

        assume

         A2: f is PartFunc of D, A;

        then f in ( PFuncs (D,A)) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is PartFunc of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is PartFunc of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = COMPLEX ;

      let D be set;

      defpred P[ object] means $1 is Function of D, A;

      :: VALUED_2:def9

      func C_Funcs (D) -> set means

      : Def9: for f be object holds f in it iff f is Function of D, COMPLEX ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is Function of D, A by A1;

        assume

         A2: f is Function of D, A;

        then f in ( Funcs (D,A)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is Function of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is Function of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = ExtREAL ;

      let D be set;

      defpred P[ object] means $1 is PartFunc of D, A;

      :: VALUED_2:def10

      func E_PFuncs (D) -> set means

      : Def10: for f be object holds f in it iff f is PartFunc of D, ExtREAL ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is PartFunc of D, A by A1;

        assume

         A2: f is PartFunc of D, A;

        then f in ( PFuncs (D,A)) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is PartFunc of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is PartFunc of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = ExtREAL ;

      let D be set;

      defpred P[ object] means $1 is Function of D, A;

      :: VALUED_2:def11

      func E_Funcs (D) -> set means

      : Def11: for f be object holds f in it iff f is Function of D, ExtREAL ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is Function of D, A by A1;

        assume

         A2: f is Function of D, A;

        then f in ( Funcs (D,A)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is Function of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is Function of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = REAL ;

      let D be set;

      defpred P[ object] means $1 is PartFunc of D, A;

      :: VALUED_2:def12

      func R_PFuncs (D) -> set means

      : Def12: for f be object holds f in it iff f is PartFunc of D, REAL ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is PartFunc of D, A by A1;

        assume

         A2: f is PartFunc of D, A;

        then f in ( PFuncs (D,A)) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is PartFunc of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is PartFunc of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = REAL ;

      let D be set;

      defpred P[ object] means $1 is Function of D, A;

      :: VALUED_2:def13

      func R_Funcs (D) -> set means

      : Def13: for f be object holds f in it iff f is Function of D, REAL ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is Function of D, A by A1;

        assume

         A2: f is Function of D, A;

        then f in ( Funcs (D,A)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is Function of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is Function of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = RAT ;

      let D be set;

      defpred P[ object] means $1 is PartFunc of D, A;

      :: VALUED_2:def14

      func Q_PFuncs (D) -> set means

      : Def14: for f be object holds f in it iff f is PartFunc of D, RAT ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is PartFunc of D, A by A1;

        assume

         A2: f is PartFunc of D, A;

        then f in ( PFuncs (D,A)) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is PartFunc of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is PartFunc of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = RAT ;

      let D be set;

      defpred P[ object] means $1 is Function of D, A;

      :: VALUED_2:def15

      func Q_Funcs (D) -> set means

      : Def15: for f be object holds f in it iff f is Function of D, RAT ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is Function of D, A by A1;

        assume

         A2: f is Function of D, A;

        then f in ( Funcs (D,A)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is Function of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is Function of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = INT ;

      let D be set;

      defpred P[ object] means $1 is PartFunc of D, A;

      :: VALUED_2:def16

      func I_PFuncs (D) -> set means

      : Def16: for f be object holds f in it iff f is PartFunc of D, INT ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is PartFunc of D, A by A1;

        assume

         A2: f is PartFunc of D, A;

        then f in ( PFuncs (D,A)) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is PartFunc of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is PartFunc of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = INT ;

      let D be set;

      defpred P[ object] means $1 is Function of D, A;

      :: VALUED_2:def17

      func I_Funcs (D) -> set means

      : Def17: for f be object holds f in it iff f is Function of D, INT ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is Function of D, A by A1;

        assume

         A2: f is Function of D, A;

        then f in ( Funcs (D,A)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is Function of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is Function of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = NAT ;

      let D be set;

      defpred P[ object] means $1 is PartFunc of D, A;

      :: VALUED_2:def18

      func N_PFuncs (D) -> set means

      : Def18: for f be object holds f in it iff f is PartFunc of D, NAT ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( PFuncs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is PartFunc of D, A by A1;

        assume

         A2: f is PartFunc of D, A;

        then f in ( PFuncs (D,A)) by PARTFUN1: 45;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is PartFunc of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is PartFunc of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    definition

      set A = NAT ;

      let D be set;

      defpred P[ object] means $1 is Function of D, A;

      :: VALUED_2:def19

      func N_Funcs (D) -> set means

      : Def19: for f be object holds f in it iff f is Function of D, NAT ;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (D,A)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let f be object;

        thus f in X implies f is Function of D, A by A1;

        assume

         A2: f is Function of D, A;

        then f in ( Funcs (D,A)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be set;

        assume for f be object holds f in P iff f is Function of D, A;

        then

         A3: for f be object holds f in P iff P[f];

        assume for f be object holds f in Q iff f is Function of D, A;

        then

         A4: for f be object holds f in Q iff P[f];

        thus P = Q from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    theorem :: VALUED_2:1

    

     Th1: ( C_Funcs X) is Subset of ( C_PFuncs X)

    proof

      ( C_Funcs X) c= ( C_PFuncs X)

      proof

        let x be object;

        assume x in ( C_Funcs X);

        then x is Function of X, COMPLEX by Def9;

        hence thesis by Def8;

      end;

      hence thesis;

    end;

    theorem :: VALUED_2:2

    

     Th2: ( E_Funcs X) is Subset of ( E_PFuncs X)

    proof

      ( E_Funcs X) c= ( E_PFuncs X)

      proof

        let x be object;

        assume x in ( E_Funcs X);

        then x is Function of X, ExtREAL by Def11;

        hence thesis by Def10;

      end;

      hence thesis;

    end;

    theorem :: VALUED_2:3

    

     Th3: ( R_Funcs X) is Subset of ( R_PFuncs X)

    proof

      ( R_Funcs X) c= ( R_PFuncs X)

      proof

        let x be object;

        assume x in ( R_Funcs X);

        then x is Function of X, REAL by Def13;

        hence thesis by Def12;

      end;

      hence thesis;

    end;

    theorem :: VALUED_2:4

    

     Th4: ( Q_Funcs X) is Subset of ( Q_PFuncs X)

    proof

      ( Q_Funcs X) c= ( Q_PFuncs X)

      proof

        let x be object;

        assume x in ( Q_Funcs X);

        then x is Function of X, RAT by Def15;

        hence thesis by Def14;

      end;

      hence thesis;

    end;

    theorem :: VALUED_2:5

    

     Th5: ( I_Funcs X) is Subset of ( I_PFuncs X)

    proof

      ( I_Funcs X) c= ( I_PFuncs X)

      proof

        let x be object;

        assume x in ( I_Funcs X);

        then x is Function of X, INT by Def17;

        hence thesis by Def16;

      end;

      hence thesis;

    end;

    theorem :: VALUED_2:6

    

     Th6: ( N_Funcs X) is Subset of ( N_PFuncs X)

    proof

      ( N_Funcs X) c= ( N_PFuncs X)

      proof

        let x be object;

        assume x in ( N_Funcs X);

        then x is Function of X, NAT by Def19;

        hence thesis by Def18;

      end;

      hence thesis;

    end;

    registration

      let X;

      cluster ( C_PFuncs X) -> complex-functions-membered;

      coherence by Def8;

      cluster ( C_Funcs X) -> complex-functions-membered;

      coherence

      proof

        reconsider C = ( C_Funcs X) as Subset of ( C_PFuncs X) by Th1;

        C is complex-functions-membered;

        hence thesis;

      end;

      cluster ( E_PFuncs X) -> ext-real-functions-membered;

      coherence by Def10;

      cluster ( E_Funcs X) -> ext-real-functions-membered;

      coherence

      proof

        reconsider C = ( E_Funcs X) as Subset of ( E_PFuncs X) by Th2;

        C is ext-real-functions-membered;

        hence thesis;

      end;

      cluster ( R_PFuncs X) -> real-functions-membered;

      coherence by Def12;

      cluster ( R_Funcs X) -> real-functions-membered;

      coherence

      proof

        reconsider C = ( R_Funcs X) as Subset of ( R_PFuncs X) by Th3;

        C is real-functions-membered;

        hence thesis;

      end;

      cluster ( Q_PFuncs X) -> rational-functions-membered;

      coherence by Def14;

      cluster ( Q_Funcs X) -> rational-functions-membered;

      coherence

      proof

        reconsider C = ( Q_Funcs X) as Subset of ( Q_PFuncs X) by Th4;

        C is rational-functions-membered;

        hence thesis;

      end;

      cluster ( I_PFuncs X) -> integer-functions-membered;

      coherence by Def16;

      cluster ( I_Funcs X) -> integer-functions-membered;

      coherence

      proof

        reconsider C = ( I_Funcs X) as Subset of ( I_PFuncs X) by Th5;

        C is integer-functions-membered;

        hence thesis;

      end;

      cluster ( N_PFuncs X) -> natural-functions-membered;

      coherence by Def18;

      cluster ( N_Funcs X) -> natural-functions-membered;

      coherence

      proof

        reconsider C = ( N_Funcs X) as Subset of ( N_PFuncs X) by Th6;

        C is natural-functions-membered;

        hence thesis;

      end;

    end

    registration

      let X be complex-functions-membered set;

      cluster -> complex-valued for Element of X;

      coherence

      proof

        X is empty or X is non empty;

        hence thesis by Def2, SUBSET_1:def 1;

      end;

    end

    registration

      let X be ext-real-functions-membered set;

      cluster -> ext-real-valued for Element of X;

      coherence

      proof

        X is empty or X is non empty;

        hence thesis by Def3, SUBSET_1:def 1;

      end;

    end

    registration

      let X be real-functions-membered set;

      cluster -> real-valued for Element of X;

      coherence

      proof

        X is empty or X is non empty;

        hence thesis by Def4, SUBSET_1:def 1;

      end;

    end

    registration

      let X be rational-functions-membered set;

      cluster -> RAT -valued for Element of X;

      coherence

      proof

        X is empty or X is non empty;

        hence thesis by Def5, SUBSET_1:def 1;

      end;

    end

    registration

      let X be integer-functions-membered set;

      cluster -> INT -valued for Element of X;

      coherence

      proof

        X is empty or X is non empty;

        hence thesis by Def6, SUBSET_1:def 1;

      end;

    end

    registration

      let X be natural-functions-membered set;

      cluster -> natural-valued for Element of X;

      coherence

      proof

        X is empty or X is non empty;

        hence thesis by Def7, SUBSET_1:def 1;

      end;

    end

    registration

      let X be set, x be object;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      cluster (f . x) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let X be set, x be object;

      let Y be ext-real-functions-membered set;

      let f be PartFunc of X, Y;

      cluster (f . x) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let X be set, x be object;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let X be set, x be object;

      let Y be ext-real-functions-membered set;

      let f be PartFunc of X, Y;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let X be set, x be object;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let X be set, x be object;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let X be set, x be object;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let X be set, x be object;

      let Y be natural-functions-membered set;

      let f be PartFunc of X, Y;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let X;

      let Y be complex-membered set;

      cluster ( PFuncs (X,Y)) -> complex-functions-membered;

      coherence

      proof

        let x;

        assume x in ( PFuncs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) c= X & ( rng f) c= Y by PARTFUN1:def 3;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be ext-real-membered set;

      cluster ( PFuncs (X,Y)) -> ext-real-functions-membered;

      coherence

      proof

        let x;

        assume x in ( PFuncs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) c= X & ( rng f) c= Y by PARTFUN1:def 3;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be real-membered set;

      cluster ( PFuncs (X,Y)) -> real-functions-membered;

      coherence

      proof

        let x;

        assume x in ( PFuncs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) c= X & ( rng f) c= Y by PARTFUN1:def 3;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be rational-membered set;

      cluster ( PFuncs (X,Y)) -> rational-functions-membered;

      coherence

      proof

        let x;

        assume x in ( PFuncs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) c= X & ( rng f) c= Y by PARTFUN1:def 3;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be integer-membered set;

      cluster ( PFuncs (X,Y)) -> integer-functions-membered;

      coherence

      proof

        let x;

        assume x in ( PFuncs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) c= X & ( rng f) c= Y by PARTFUN1:def 3;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be natural-membered set;

      cluster ( PFuncs (X,Y)) -> natural-functions-membered;

      coherence

      proof

        let x;

        assume x in ( PFuncs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) c= X & ( rng f) c= Y by PARTFUN1:def 3;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be complex-membered set;

      cluster ( Funcs (X,Y)) -> complex-functions-membered;

      coherence

      proof

        let x;

        assume x in ( Funcs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be ext-real-membered set;

      cluster ( Funcs (X,Y)) -> ext-real-functions-membered;

      coherence

      proof

        let x;

        assume x in ( Funcs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be real-membered set;

      cluster ( Funcs (X,Y)) -> real-functions-membered;

      coherence

      proof

        let x;

        assume x in ( Funcs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be rational-membered set;

      cluster ( Funcs (X,Y)) -> rational-functions-membered;

      coherence

      proof

        let x;

        assume x in ( Funcs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be integer-membered set;

      cluster ( Funcs (X,Y)) -> integer-functions-membered;

      coherence

      proof

        let x;

        assume x in ( Funcs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    registration

      let X;

      let Y be natural-membered set;

      cluster ( Funcs (X,Y)) -> natural-functions-membered;

      coherence

      proof

        let x;

        assume x in ( Funcs (X,Y));

        then

        consider f be Function such that

         A1: x = f and

         A2: ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        reconsider f as PartFunc of X, Y by A2, RELSET_1: 4;

        f is set;

        hence thesis by A1;

      end;

    end

    definition

      let R be Relation;

      :: VALUED_2:def20

      attr R is complex-functions-valued means

      : Def20: ( rng R) is complex-functions-membered;

      :: VALUED_2:def21

      attr R is ext-real-functions-valued means

      : Def21: ( rng R) is ext-real-functions-membered;

      :: VALUED_2:def22

      attr R is real-functions-valued means

      : Def22: ( rng R) is real-functions-membered;

      :: VALUED_2:def23

      attr R is rational-functions-valued means

      : Def23: ( rng R) is rational-functions-membered;

      :: VALUED_2:def24

      attr R is integer-functions-valued means

      : Def24: ( rng R) is integer-functions-membered;

      :: VALUED_2:def25

      attr R is natural-functions-valued means

      : Def25: ( rng R) is natural-functions-membered;

    end

    registration

      let Y be complex-functions-membered set;

      cluster -> complex-functions-valued for Y -valued Function;

      coherence

      proof

        let f be Y -valued Function;

        thus ( rng f) is complex-functions-membered;

      end;

    end

    definition

      let f be Function;

      :: original: complex-functions-valued

      redefine

      :: VALUED_2:def26

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

      compatibility

      proof

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

        proof

          assume

           A1: ( rng f) is complex-functions-membered;

          let x;

          assume x in ( dom f);

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

          hence thesis by A1;

        end;

        assume

         A2: for x be object st x in ( dom f) holds (f . x) is complex-valued Function;

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A2;

      end;

      :: original: ext-real-functions-valued

      redefine

      :: VALUED_2:def27

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

      compatibility

      proof

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

        proof

          assume

           A3: ( rng f) is ext-real-functions-membered;

          let x;

          assume x in ( dom f);

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

          hence thesis by A3;

        end;

        assume

         A4: for x be object st x in ( dom f) holds (f . x) is ext-real-valued Function;

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A4;

      end;

      :: original: real-functions-valued

      redefine

      :: VALUED_2:def28

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

      compatibility

      proof

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

        proof

          assume

           A5: ( rng f) is real-functions-membered;

          let x;

          assume x in ( dom f);

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

          hence thesis by A5;

        end;

        assume

         A6: for x be object st x in ( dom f) holds (f . x) is real-valued Function;

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A6;

      end;

      :: original: rational-functions-valued

      redefine

      :: VALUED_2:def29

      attr f is rational-functions-valued means for x be object st x in ( dom f) holds (f . x) is RAT -valued Function;

      compatibility

      proof

        thus f is rational-functions-valued implies for x be object st x in ( dom f) holds (f . x) is RAT -valued Function

        proof

          assume

           A7: ( rng f) is rational-functions-membered;

          let x;

          assume x in ( dom f);

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

          hence thesis by A7;

        end;

        assume

         A8: for x be object st x in ( dom f) holds (f . x) is RAT -valued Function;

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A8;

      end;

      :: original: integer-functions-valued

      redefine

      :: VALUED_2:def30

      attr f is integer-functions-valued means for x be object st x in ( dom f) holds (f . x) is INT -valued Function;

      compatibility

      proof

        thus f is integer-functions-valued implies for x be object st x in ( dom f) holds (f . x) is INT -valued Function

        proof

          assume

           A9: ( rng f) is integer-functions-membered;

          let x;

          assume x in ( dom f);

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

          hence thesis by A9;

        end;

        assume

         A10: for x be object st x in ( dom f) holds (f . x) is INT -valued Function;

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A10;

      end;

      :: original: natural-functions-valued

      redefine

      :: VALUED_2:def31

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

      compatibility

      proof

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

        proof

          assume

           A11: ( rng f) is natural-functions-membered;

          let x;

          assume x in ( dom f);

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

          hence thesis by A11;

        end;

        assume

         A12: for x be object st x in ( dom f) holds (f . x) is natural-valued Function;

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A12;

      end;

    end

    registration

      cluster natural-functions-valued -> integer-functions-valued for Relation;

      coherence ;

      cluster integer-functions-valued -> rational-functions-valued for Relation;

      coherence ;

      cluster rational-functions-valued -> real-functions-valued for Relation;

      coherence ;

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

      coherence ;

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

      coherence ;

    end

    registration

      cluster empty -> natural-functions-valued for Relation;

      coherence ;

    end

    registration

      cluster natural-functions-valued for Function;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let R be complex-functions-valued Relation;

      cluster ( rng R) -> complex-functions-membered;

      coherence by Def20;

    end

    registration

      let R be ext-real-functions-valued Relation;

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

      coherence by Def21;

    end

    registration

      let R be real-functions-valued Relation;

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

      coherence by Def22;

    end

    registration

      let R be rational-functions-valued Relation;

      cluster ( rng R) -> rational-functions-membered;

      coherence by Def23;

    end

    registration

      let R be integer-functions-valued Relation;

      cluster ( rng R) -> integer-functions-membered;

      coherence by Def24;

    end

    registration

      let R be natural-functions-valued Relation;

      cluster ( rng R) -> natural-functions-membered;

      coherence by Def25;

    end

    registration

      let X;

      let Y be complex-functions-membered set;

      cluster -> complex-functions-valued for PartFunc of X, Y;

      coherence ;

    end

    registration

      let X;

      let Y be ext-real-functions-membered set;

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

      coherence ;

    end

    registration

      let X;

      let Y be real-functions-membered set;

      cluster -> real-functions-valued for PartFunc of X, Y;

      coherence ;

    end

    registration

      let X;

      let Y be rational-functions-membered set;

      cluster -> rational-functions-valued for PartFunc of X, Y;

      coherence ;

    end

    registration

      let X;

      let Y be integer-functions-membered set;

      cluster -> integer-functions-valued for PartFunc of X, Y;

      coherence ;

    end

    registration

      let X;

      let Y be natural-functions-membered set;

      cluster -> natural-functions-valued for PartFunc of X, Y;

      coherence ;

    end

    registration

      cluster complex-functions-valued -> Function-yielding for Function;

      coherence

      proof

        let f be Function such that

         A1: f is complex-functions-valued;

        let x be object;

        thus thesis by A1;

      end;

      cluster real-functions-valued -> Function-yielding for Function;

      coherence ;

      cluster ext-real-functions-valued -> Function-yielding for Function;

      coherence

      proof

        let f be Function such that

         A2: f is ext-real-functions-valued;

        let x be object;

        thus thesis by A2;

      end;

    end

    registration

      let f be complex-functions-valued Function;

      let x be object;

      cluster (f . x) -> Function-like Relation-like;

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be ext-real-functions-valued Function;

      let x be object;

      cluster (f . x) -> Function-like Relation-like;

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be complex-functions-valued Function;

      let x be object;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be ext-real-functions-valued Function;

      let x be object;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be real-functions-valued Function;

      let x be object;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be rational-functions-valued Function;

      let x be object;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be integer-functions-valued Function;

      let x be object;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be natural-functions-valued Function;

      let x be object;

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

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

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

          hence thesis;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let f be real-functions-valued Function;

      let x, y;

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

      coherence ;

    end

    begin

    reserve Y,Y1,Y2 for complex-functions-membered set,

c,c1,c2 for Complex,

f for PartFunc of X, Y,

f1 for PartFunc of X1, Y1,

f2 for PartFunc of X2, Y2,

g,h,k for complex-valued Function;

    theorem :: VALUED_2:7

    

     Th7: g <> {} & (g + c1) = (g + c2) implies c1 = c2

    proof

      assume that

       A1: g <> {} and

       A2: (g + c1) = (g + c2);

      consider x be object such that

       A3: x in ( dom g) by A1, XBOOLE_0:def 1;

      ( dom g) = ( dom (g + c2)) by VALUED_1:def 2;

      then

       A4: ((g + c2) . x) = ((g . x) + c2) by A3, VALUED_1:def 2;

      ( dom g) = ( dom (g + c1)) by VALUED_1:def 2;

      then ((g + c1) . x) = ((g . x) + c1) by A3, VALUED_1:def 2;

      hence c1 = c2 by A2, A4;

    end;

    theorem :: VALUED_2:8

    

     Th8: g <> {} & (g - c1) = (g - c2) implies c1 = c2

    proof

      assume that

       A1: g <> {} and

       A2: (g - c1) = (g - c2);

      consider x be object such that

       A3: x in ( dom g) by A1, XBOOLE_0:def 1;

      ( dom g) = ( dom (g - c2)) by VALUED_1:def 2;

      then

       A4: ((g - c2) . x) = ((g . x) - c2) by A3, VALUED_1:def 2;

      ( dom g) = ( dom (g - c1)) by VALUED_1:def 2;

      then ((g - c1) . x) = ((g . x) - c1) by A3, VALUED_1:def 2;

      hence c1 = c2 by A2, A4;

    end;

    theorem :: VALUED_2:9

    

     Th9: g <> {} & g is non-empty & (g (#) c1) = (g (#) c2) implies c1 = c2

    proof

      assume that

       A1: g <> {} and

       A2: g is non-empty and

       A3: (g (#) c1) = (g (#) c2);

      consider x be object such that

       A4: x in ( dom g) by A1, XBOOLE_0:def 1;

      (g . x) in ( rng g) by A4, FUNCT_1:def 3;

      then

       A5: (g . x) <> {} by A2, RELAT_1:def 9;

      ((g (#) c1) . x) = ((g . x) * c1) & ((g (#) c2) . x) = ((g . x) * c2) by VALUED_1: 6;

      hence c1 = c2 by A3, A5, XCMPLX_1: 5;

    end;

    theorem :: VALUED_2:10

    

     Th10: ( - (g + c)) = (( - g) - c)

    proof

      

       A1: ( dom ( - (g + c))) = ( dom (g + c)) by VALUED_1: 8;

      

       A2: ( dom (g + c)) = ( dom g) & ( dom (( - g) - c)) = ( dom ( - g)) by VALUED_1:def 2;

      hence ( dom ( - (g + c))) = ( dom (( - g) - c)) by A1, VALUED_1: 8;

      let x be object;

      assume

       A3: x in ( dom ( - (g + c)));

      

       A4: ( dom ( - g)) = ( dom g) by VALUED_1: 8;

      

      thus (( - (g + c)) . x) = ( - ((g + c) . x)) by VALUED_1: 8

      .= ( - ((g . x) + c)) by A1, A3, VALUED_1:def 2

      .= (( - (g . x)) - c)

      .= ((( - g) . x) - c) by VALUED_1: 8

      .= ((( - g) - c) . x) by A2, A1, A4, A3, VALUED_1:def 2;

    end;

    theorem :: VALUED_2:11

    

     Th11: ( - (g - c)) = (( - g) + c)

    proof

      

       A1: ( dom ( - (g - c))) = ( dom (g - c)) by VALUED_1: 8;

      

       A2: ( dom (g - c)) = ( dom g) & ( dom (( - g) + c)) = ( dom ( - g)) by VALUED_1:def 2;

      hence ( dom ( - (g - c))) = ( dom (( - g) + c)) by A1, VALUED_1: 8;

      let x be object;

      assume

       A3: x in ( dom ( - (g - c)));

      

       A4: ( dom ( - g)) = ( dom g) by VALUED_1: 8;

      

      thus (( - (g - c)) . x) = ( - ((g - c) . x)) by VALUED_1: 8

      .= ( - ((g . x) - c)) by A1, A3, VALUED_1:def 2

      .= (( - (g . x)) + c)

      .= ((( - g) . x) + c) by VALUED_1: 8

      .= ((( - g) + c) . x) by A2, A1, A4, A3, VALUED_1:def 2;

    end;

    theorem :: VALUED_2:12

    

     Th12: ((g + c1) + c2) = (g + (c1 + c2))

    proof

      

       A1: ( dom ((g + c1) + c2)) = ( dom (g + c1)) by VALUED_1:def 2;

      

       A2: ( dom (g + c1)) = ( dom g) by VALUED_1:def 2;

      hence ( dom ((g + c1) + c2)) = ( dom (g + (c1 + c2))) by A1, VALUED_1:def 2;

      let x be object;

      

       A3: ( dom (g + (c1 + c2))) = ( dom g) by VALUED_1:def 2;

      assume

       A4: x in ( dom ((g + c1) + c2));

      

      hence (((g + c1) + c2) . x) = (((g + c1) . x) + c2) by VALUED_1:def 2

      .= (((g . x) + c1) + c2) by A1, A4, VALUED_1:def 2

      .= ((g . x) + (c1 + c2))

      .= ((g + (c1 + c2)) . x) by A1, A2, A3, A4, VALUED_1:def 2;

    end;

    theorem :: VALUED_2:13

    

     Th13: ((g + c1) - c2) = (g + (c1 - c2))

    proof

      

       A1: ( dom ((g + c1) - c2)) = ( dom (g + c1)) by VALUED_1:def 2;

      

       A2: ( dom (g + c1)) = ( dom g) by VALUED_1:def 2;

      hence ( dom ((g + c1) - c2)) = ( dom (g + (c1 - c2))) by A1, VALUED_1:def 2;

      let x be object;

      

       A3: ( dom (g + (c1 - c2))) = ( dom g) by VALUED_1:def 2;

      assume

       A4: x in ( dom ((g + c1) - c2));

      

      hence (((g + c1) - c2) . x) = (((g + c1) . x) - c2) by VALUED_1:def 2

      .= (((g . x) + c1) - c2) by A1, A4, VALUED_1:def 2

      .= ((g . x) + (c1 - c2))

      .= ((g + (c1 - c2)) . x) by A1, A2, A3, A4, VALUED_1:def 2;

    end;

    theorem :: VALUED_2:14

    

     Th14: ((g - c1) + c2) = (g - (c1 - c2))

    proof

      

       A1: ( dom ((g - c1) + c2)) = ( dom (g - c1)) by VALUED_1:def 2;

      

       A2: ( dom (g - c1)) = ( dom g) by VALUED_1:def 2;

      hence ( dom ((g - c1) + c2)) = ( dom (g - (c1 - c2))) by A1, VALUED_1:def 2;

      let x be object;

      

       A3: ( dom (g - (c1 - c2))) = ( dom g) by VALUED_1:def 2;

      assume

       A4: x in ( dom ((g - c1) + c2));

      

      hence (((g - c1) + c2) . x) = (((g - c1) . x) + c2) by VALUED_1:def 2

      .= (((g . x) - c1) + c2) by A1, A4, VALUED_1:def 2

      .= ((g . x) - (c1 - c2))

      .= ((g - (c1 - c2)) . x) by A1, A2, A3, A4, VALUED_1:def 2;

    end;

    theorem :: VALUED_2:15

    

     Th15: ((g - c1) - c2) = (g - (c1 + c2))

    proof

      

       A1: ( dom ((g - c1) - c2)) = ( dom (g - c1)) by VALUED_1:def 2;

      

       A2: ( dom (g - c1)) = ( dom g) by VALUED_1:def 2;

      hence ( dom ((g - c1) - c2)) = ( dom (g - (c1 + c2))) by A1, VALUED_1:def 2;

      let x be object;

      

       A3: ( dom (g - (c1 + c2))) = ( dom g) by VALUED_1:def 2;

      assume

       A4: x in ( dom ((g - c1) - c2));

      

      hence (((g - c1) - c2) . x) = (((g - c1) . x) - c2) by VALUED_1:def 2

      .= (((g . x) - c1) - c2) by A1, A4, VALUED_1:def 2

      .= ((g . x) - (c1 + c2))

      .= ((g - (c1 + c2)) . x) by A1, A2, A3, A4, VALUED_1:def 2;

    end;

    theorem :: VALUED_2:16

    

     Th16: ((g (#) c1) (#) c2) = (g (#) (c1 * c2))

    proof

      ( dom ((g (#) c1) (#) c2)) = ( dom (g (#) c1)) & ( dom (g (#) c1)) = ( dom g) by VALUED_1:def 5;

      hence ( dom ((g (#) c1) (#) c2)) = ( dom (g (#) (c1 * c2))) by VALUED_1:def 5;

      let x be object;

      assume x in ( dom ((g (#) c1) (#) c2));

      

      thus (((g (#) c1) (#) c2) . x) = (((g (#) c1) . x) * c2) by VALUED_1: 6

      .= (((g . x) * c1) * c2) by VALUED_1: 6

      .= ((g . x) * (c1 * c2))

      .= ((g (#) (c1 * c2)) . x) by VALUED_1: 6;

    end;

    theorem :: VALUED_2:17

    

     Th17: ( - (g + h)) = (( - g) - h)

    proof

      

       A1: ( dom ( - (g + h))) = ( dom (g + h)) by VALUED_1: 8;

      ( dom (g + h)) = (( dom g) /\ ( dom h)) & ( dom (( - g) - h)) = (( dom ( - g)) /\ ( dom h)) by VALUED_1: 12, VALUED_1:def 1;

      hence

       A2: ( dom ( - (g + h))) = ( dom (( - g) - h)) by A1, VALUED_1: 8;

      let x be object;

      assume

       A3: x in ( dom ( - (g + h)));

      

      thus (( - (g + h)) . x) = ( - ((g + h) . x)) by VALUED_1: 8

      .= ( - ((g . x) + (h . x))) by A1, A3, VALUED_1:def 1

      .= (( - (g . x)) - (h . x))

      .= ((( - g) . x) - (h . x)) by VALUED_1: 8

      .= ((( - g) - h) . x) by A2, A3, VALUED_1: 13;

    end;

    theorem :: VALUED_2:18

    

     Th18: (g - h) = ( - (h - g))

    proof

      

       A1: ( dom ( - (h - g))) = ( dom (h - g)) by VALUED_1: 8;

      ( dom (g - h)) = (( dom g) /\ ( dom h)) by VALUED_1: 12;

      hence

       A2: ( dom (g - h)) = ( dom ( - (h - g))) by A1, VALUED_1: 12;

      let x be object;

      assume

       A3: x in ( dom (g - h));

      

      hence ((g - h) . x) = ((g . x) - (h . x)) by VALUED_1: 13

      .= ( - ((h . x) - (g . x)))

      .= ( - ((h - g) . x)) by A1, A2, A3, VALUED_1: 13

      .= (( - (h - g)) . x) by VALUED_1: 8;

    end;

    theorem :: VALUED_2:19

    

     Th19: ((g (#) h) /" k) = (g (#) (h /" k))

    proof

      

       A1: ( dom (g (#) (h /" k))) = (( dom g) /\ ( dom (h /" k))) & ( dom ((g (#) h) /" k)) = (( dom (g (#) h)) /\ ( dom k)) by VALUED_1: 16, VALUED_1:def 4;

      ( dom (g (#) h)) = (( dom g) /\ ( dom h)) & ( dom (h /" k)) = (( dom h) /\ ( dom k)) by VALUED_1: 16, VALUED_1:def 4;

      hence ( dom ((g (#) h) /" k)) = ( dom (g (#) (h /" k))) by A1, XBOOLE_1: 16;

      let x be object;

      assume x in ( dom ((g (#) h) /" k));

      

      thus (((g (#) h) /" k) . x) = (((g (#) h) . x) / (k . x)) by VALUED_1: 17

      .= (((g . x) * (h . x)) / (k . x)) by VALUED_1: 5

      .= ((g . x) * ((h . x) / (k . x)))

      .= ((g . x) * ((h /" k) . x)) by VALUED_1: 17

      .= ((g (#) (h /" k)) . x) by VALUED_1: 5;

    end;

    theorem :: VALUED_2:20

    

     Th20: ((g /" h) (#) k) = ((g (#) k) /" h)

    proof

      

       A1: ( dom ((g /" h) (#) k)) = (( dom (g /" h)) /\ ( dom k)) & ( dom ((g (#) k) /" h)) = (( dom (g (#) k)) /\ ( dom h)) by VALUED_1: 16, VALUED_1:def 4;

      ( dom (g /" h)) = (( dom g) /\ ( dom h)) & ( dom (g (#) k)) = (( dom g) /\ ( dom k)) by VALUED_1: 16, VALUED_1:def 4;

      hence ( dom ((g /" h) (#) k)) = ( dom ((g (#) k) /" h)) by A1, XBOOLE_1: 16;

      let x be object;

      assume x in ( dom ((g /" h) (#) k));

      

      thus (((g /" h) (#) k) . x) = (((g /" h) . x) * (k . x)) by VALUED_1: 5

      .= (((g . x) / (h . x)) * (k . x)) by VALUED_1: 17

      .= (((g . x) * (k . x)) / (h . x))

      .= (((g (#) k) . x) / (h . x)) by VALUED_1: 5

      .= (((g (#) k) /" h) . x) by VALUED_1: 17;

    end;

    theorem :: VALUED_2:21

    

     Th21: ((g /" h) /" k) = (g /" (h (#) k))

    proof

      

       A1: ( dom ((g /" h) /" k)) = (( dom (g /" h)) /\ ( dom k)) & ( dom (g /" (h (#) k))) = (( dom g) /\ ( dom (h (#) k))) by VALUED_1: 16;

      ( dom (g /" h)) = (( dom g) /\ ( dom h)) & ( dom (h (#) k)) = (( dom h) /\ ( dom k)) by VALUED_1: 16, VALUED_1:def 4;

      hence ( dom ((g /" h) /" k)) = ( dom (g /" (h (#) k))) by A1, XBOOLE_1: 16;

      let x be object;

      assume x in ( dom ((g /" h) /" k));

      

      thus (((g /" h) /" k) . x) = (((g /" h) . x) / (k . x)) by VALUED_1: 17

      .= (((g . x) / (h . x)) / (k . x)) by VALUED_1: 17

      .= ((g . x) / ((h . x) * (k . x))) by XCMPLX_1: 78

      .= ((g . x) / ((h (#) k) . x)) by VALUED_1: 5

      .= ((g /" (h (#) k)) . x) by VALUED_1: 17;

    end;

    theorem :: VALUED_2:22

    

     Th22: (c (#) ( - g)) = (( - c) (#) g)

    proof

      ( dom (c (#) ( - g))) = ( dom ( - g)) by VALUED_1:def 5

      .= ( dom g) by VALUED_1: 8;

      hence ( dom (c (#) ( - g))) = ( dom (( - c) (#) g)) by VALUED_1:def 5;

      let x be object;

      assume x in ( dom (c (#) ( - g)));

      

      thus ((c (#) ( - g)) . x) = (c * (( - g) . x)) by VALUED_1: 6

      .= (c * ( - (g . x))) by VALUED_1: 8

      .= (( - c) * (g . x))

      .= ((( - c) (#) g) . x) by VALUED_1: 6;

    end;

    theorem :: VALUED_2:23

    

     Th23: (c (#) ( - g)) = ( - (c (#) g))

    proof

      

       A1: ( dom ( - (c (#) g))) = ( dom (c (#) g)) by VALUED_1: 8

      .= ( dom g) by VALUED_1:def 5;

      ( dom (c (#) ( - g))) = ( dom ( - g)) by VALUED_1:def 5

      .= ( dom g) by VALUED_1: 8;

      hence ( dom (c (#) ( - g))) = ( dom ( - (c (#) g))) by A1;

      let x be object;

      assume x in ( dom (c (#) ( - g)));

      

      thus ((c (#) ( - g)) . x) = (c * (( - g) . x)) by VALUED_1: 6

      .= (c * ( - (g . x))) by VALUED_1: 8

      .= ( - (c * (g . x)))

      .= ( - ((c (#) g) . x)) by VALUED_1: 6

      .= (( - (c (#) g)) . x) by VALUED_1: 8;

    end;

    theorem :: VALUED_2:24

    

     Th24: (( - c) (#) g) = ( - (c (#) g))

    proof

      

      thus (( - c) (#) g) = (c (#) ( - g)) by Th22

      .= ( - (c (#) g)) by Th23;

    end;

    theorem :: VALUED_2:25

    

     Th25: ( - (g (#) h)) = (( - g) (#) h)

    proof

      

       A1: ( dom ( - (g (#) h))) = ( dom (g (#) h)) by VALUED_1: 8;

      ( dom (g (#) h)) = (( dom g) /\ ( dom h)) & ( dom (( - g) (#) h)) = (( dom ( - g)) /\ ( dom h)) by VALUED_1:def 4;

      hence ( dom ( - (g (#) h))) = ( dom (( - g) (#) h)) by A1, VALUED_1: 8;

      let x be object;

      assume x in ( dom ( - (g (#) h)));

      

      thus (( - (g (#) h)) . x) = ( - ((g (#) h) . x)) by VALUED_1: 8

      .= ( - ((g . x) * (h . x))) by VALUED_1: 5

      .= (( - (g . x)) * (h . x))

      .= ((( - g) . x) * (h . x)) by VALUED_1: 8

      .= ((( - g) (#) h) . x) by VALUED_1: 5;

    end;

    theorem :: VALUED_2:26

    ( - (g /" h)) = (( - g) /" h)

    proof

      

       A1: ( dom ( - (g /" h))) = ( dom (g /" h)) by VALUED_1: 8;

      ( dom (g /" h)) = (( dom g) /\ ( dom h)) & ( dom (( - g) /" h)) = (( dom ( - g)) /\ ( dom h)) by VALUED_1: 16;

      hence ( dom ( - (g /" h))) = ( dom (( - g) /" h)) by A1, VALUED_1: 8;

      let x be object;

      assume x in ( dom ( - (g /" h)));

      

      thus (( - (g /" h)) . x) = ( - ((g /" h) . x)) by VALUED_1: 8

      .= ( - ((g . x) / (h . x))) by VALUED_1: 17

      .= (( - (g . x)) / (h . x))

      .= ((( - g) . x) / (h . x)) by VALUED_1: 8

      .= ((( - g) /" h) . x) by VALUED_1: 17;

    end;

    theorem :: VALUED_2:27

    

     Th27: ( - (g /" h)) = (g /" ( - h))

    proof

      

       A1: ( dom ( - h)) = ( dom h) by VALUED_1: 8;

      ( dom (g /" h)) = (( dom g) /\ ( dom h)) & ( dom (g /" ( - h))) = (( dom g) /\ ( dom ( - h))) by VALUED_1: 16;

      hence ( dom ( - (g /" h))) = ( dom (g /" ( - h))) by A1, VALUED_1: 8;

      let x be object;

      assume x in ( dom ( - (g /" h)));

      

      thus (( - (g /" h)) . x) = ( - ((g /" h) . x)) by VALUED_1: 8

      .= ( - ((g . x) / (h . x))) by VALUED_1: 17

      .= ((g . x) / ( - (h . x))) by XCMPLX_1: 188

      .= ((g . x) / (( - h) . x)) by VALUED_1: 8

      .= ((g /" ( - h)) . x) by VALUED_1: 17;

    end;

    definition

      let f be complex-valued Function, c be Complex;

      :: VALUED_2:def32

      func f (/) c -> Function equals ((1 / c) (#) f);

      coherence ;

    end

    registration

      let f be complex-valued Function, c be Complex;

      cluster (f (/) c) -> complex-valued;

      coherence ;

    end

    registration

      let f be real-valued Function, r be Real;

      cluster (f (/) r) -> real-valued;

      coherence ;

    end

    registration

      let f be RAT -valued Function, r be Rational;

      cluster (f (/) r) -> RAT -valued;

      coherence ;

    end

    registration

      let f be complex-valued FinSequence, c be Complex;

      cluster (f (/) c) -> FinSequence-like;

      coherence ;

    end

    theorem :: VALUED_2:28

    ( dom (g (/) c)) = ( dom g) by VALUED_1:def 5;

    theorem :: VALUED_2:29

    for x be object holds ((g (/) c) . x) = ((g . x) / c) by VALUED_1: 6;

    theorem :: VALUED_2:30

    

     Th30: (( - g) (/) c) = ( - (g (/) c))

    proof

      

      thus (( - g) (/) c) = (( - (1 / c)) (#) g) by Th22

      .= ( - (g (/) c)) by Th24;

    end;

    theorem :: VALUED_2:31

    

     Th31: (g (/) ( - c)) = ( - (g (/) c))

    proof

      

      thus (g (/) ( - c)) = (( - (1 / c)) (#) g) by XCMPLX_1: 188

      .= ( - (g (/) c)) by Th24;

    end;

    theorem :: VALUED_2:32

    (g (/) ( - c)) = (( - g) (/) c)

    proof

      

      thus (g (/) ( - c)) = ( - (g (/) c)) by Th31

      .= (( - g) (/) c) by Th30;

    end;

    theorem :: VALUED_2:33

    

     Th33: g <> {} & g is non-empty & (g (/) c1) = (g (/) c2) implies c1 = c2

    proof

      assume that

       A1: g <> {} and

       A2: g is non-empty and

       A3: (g (/) c1) = (g (/) c2);

      consider x be object such that

       A4: x in ( dom g) by A1, XBOOLE_0:def 1;

      (g . x) in ( rng g) by A4, FUNCT_1:def 3;

      then

       A5: (g . x) <> {} by A2, RELAT_1:def 9;

      ((g (/) c1) . x) = ((g . x) / c1) & ((g (/) c2) . x) = ((g . x) / c2) by VALUED_1: 6;

      then (c1 " ) = (c2 " ) by A3, A5, XCMPLX_1: 5;

      hence c1 = c2 by XCMPLX_1: 201;

    end;

    theorem :: VALUED_2:34

    ((g (#) c1) (/) c2) = (g (#) (c1 / c2))

    proof

      ( dom (g (#) c1)) = ( dom g) & ( dom ((g (#) c1) (/) c2)) = ( dom (g (#) c1)) by VALUED_1:def 5;

      hence ( dom ((g (#) c1) (/) c2)) = ( dom (g (#) (c1 / c2))) by VALUED_1:def 5;

      let x be object;

      assume x in ( dom ((g (#) c1) (/) c2));

      

      thus (((g (#) c1) (/) c2) . x) = (((g (#) c1) . x) * (c2 " )) by VALUED_1: 6

      .= (((g . x) * c1) * (c2 " )) by VALUED_1: 6

      .= ((g . x) * (c1 / c2))

      .= ((g (#) (c1 / c2)) . x) by VALUED_1: 6;

    end;

    theorem :: VALUED_2:35

    ((g (/) c1) (#) c2) = ((g (#) c2) (/) c1)

    proof

      

       A1: ( dom ((g (/) c1) (#) c2)) = ( dom (g (/) c1)) by VALUED_1:def 5;

      ( dom (g (/) c1)) = ( dom g) & ( dom (g (#) c2)) = ( dom g) by VALUED_1:def 5;

      hence ( dom ((g (/) c1) (#) c2)) = ( dom ((g (#) c2) (/) c1)) by A1, VALUED_1:def 5;

      let x be object;

      assume x in ( dom ((g (/) c1) (#) c2));

      

      thus (((g (/) c1) (#) c2) . x) = (((g (/) c1) . x) * c2) by VALUED_1: 6

      .= (((g . x) * (c1 " )) * c2) by VALUED_1: 6

      .= (((g . x) * c2) * (c1 " ))

      .= (((g (#) c2) . x) * (c1 " )) by VALUED_1: 6

      .= (((g (#) c2) (/) c1) . x) by VALUED_1: 6;

    end;

    theorem :: VALUED_2:36

    ((g (/) c1) (/) c2) = (g (/) (c1 * c2))

    proof

      ( dom (g (/) c1)) = ( dom g) & ( dom (g (/) (c1 * c2))) = ( dom g) by VALUED_1:def 5;

      hence ( dom ((g (/) c1) (/) c2)) = ( dom (g (/) (c1 * c2))) by VALUED_1:def 5;

      let x be object;

      assume x in ( dom ((g (/) c1) (/) c2));

      

      thus (((g (/) c1) (/) c2) . x) = (((g (/) c1) . x) * (c2 " )) by VALUED_1: 6

      .= (((g . x) * (c1 " )) * (c2 " )) by VALUED_1: 6

      .= ((g . x) * ((c1 " ) * (c2 " )))

      .= ((g . x) * ((c1 * c2) " )) by XCMPLX_1: 204

      .= ((g (/) (c1 * c2)) . x) by VALUED_1: 6;

    end;

    theorem :: VALUED_2:37

    ((g + h) (/) c) = ((g (/) c) + (h (/) c))

    proof

      

       A1: ( dom ((g + h) (/) c)) = ( dom (g + h)) by VALUED_1:def 5;

      

       A2: ( dom (g + h)) = (( dom g) /\ ( dom h)) by VALUED_1:def 1;

      ( dom (g (/) c)) = ( dom g) & ( dom (h (/) c)) = ( dom h) by VALUED_1:def 5;

      hence

       A3: ( dom ((g + h) (/) c)) = ( dom ((g (/) c) + (h (/) c))) by A1, A2, VALUED_1:def 1;

      let x be object;

      assume

       A4: x in ( dom ((g + h) (/) c));

      

      thus (((g + h) (/) c) . x) = (((g + h) . x) * (c " )) by VALUED_1: 6

      .= (((g . x) + (h . x)) * (c " )) by A1, A4, VALUED_1:def 1

      .= (((g . x) * (c " )) + ((h . x) * (c " )))

      .= (((g (/) c) . x) + ((h . x) * (c " ))) by VALUED_1: 6

      .= (((g (/) c) . x) + ((h (/) c) . x)) by VALUED_1: 6

      .= (((g (/) c) + (h (/) c)) . x) by A3, A4, VALUED_1:def 1;

    end;

    theorem :: VALUED_2:38

    ((g - h) (/) c) = ((g (/) c) - (h (/) c))

    proof

      

       A1: ( dom ((g - h) (/) c)) = ( dom (g - h)) by VALUED_1:def 5;

      

       A2: ( dom (g - h)) = (( dom g) /\ ( dom h)) by VALUED_1: 12;

      ( dom (g (/) c)) = ( dom g) & ( dom (h (/) c)) = ( dom h) by VALUED_1:def 5;

      hence

       A3: ( dom ((g - h) (/) c)) = ( dom ((g (/) c) - (h (/) c))) by A1, A2, VALUED_1: 12;

      let x be object;

      assume

       A4: x in ( dom ((g - h) (/) c));

      

      thus (((g - h) (/) c) . x) = (((g - h) . x) * (c " )) by VALUED_1: 6

      .= (((g . x) - (h . x)) * (c " )) by A1, A4, VALUED_1: 13

      .= (((g . x) * (c " )) - ((h . x) * (c " )))

      .= (((g (/) c) . x) - ((h . x) * (c " ))) by VALUED_1: 6

      .= (((g (/) c) . x) - ((h (/) c) . x)) by VALUED_1: 6

      .= (((g (/) c) - (h (/) c)) . x) by A3, A4, VALUED_1: 13;

    end;

    theorem :: VALUED_2:39

    ((g (#) h) (/) c) = (g (#) (h (/) c))

    proof

      

       A1: ( dom ((g (#) h) (/) c)) = ( dom (g (#) h)) by VALUED_1:def 5;

      ( dom (g (#) h)) = (( dom g) /\ ( dom h)) & ( dom (h (/) c)) = ( dom h) by VALUED_1:def 4, VALUED_1:def 5;

      hence ( dom ((g (#) h) (/) c)) = ( dom (g (#) (h (/) c))) by A1, VALUED_1:def 4;

      let x be object;

      assume x in ( dom ((g (#) h) (/) c));

      

      thus (((g (#) h) (/) c) . x) = (((g (#) h) . x) * (c " )) by VALUED_1: 6

      .= (((g . x) * (h . x)) * (c " )) by VALUED_1: 5

      .= ((g . x) * ((h . x) * (c " )))

      .= ((g . x) * ((h (/) c) . x)) by VALUED_1: 6

      .= ((g (#) (h (/) c)) . x) by VALUED_1: 5;

    end;

    theorem :: VALUED_2:40

    ((g /" h) (/) c) = (g /" (h (#) c))

    proof

      

       A1: ( dom ((g /" h) (/) c)) = ( dom (g /" h)) by VALUED_1:def 5;

      ( dom (g /" h)) = (( dom g) /\ ( dom h)) & ( dom (h (#) c)) = ( dom h) by VALUED_1: 16, VALUED_1:def 5;

      hence ( dom ((g /" h) (/) c)) = ( dom (g /" (h (#) c))) by A1, VALUED_1: 16;

      let x be object;

      assume x in ( dom ((g /" h) (/) c));

      

      thus (((g /" h) (/) c) . x) = (((g /" h) . x) * (c " )) by VALUED_1: 6

      .= (((g . x) / (h . x)) / c) by VALUED_1: 17

      .= ((g . x) / ((h . x) * c)) by XCMPLX_1: 78

      .= ((g . x) / ((h (#) c) . x)) by VALUED_1: 6

      .= ((g /" (h (#) c)) . x) by VALUED_1: 17;

    end;

    definition

      let f be complex-functions-valued Function;

      deffunc F( object) = ( - (f . $1));

      :: VALUED_2:def33

      func <-> f -> Function means

      : Def33: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = ( - (f . x));

      existence

      proof

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = ( dom f) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = ( dom f) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: <->

      redefine

      func <-> f -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( <-> f);

        

         A1: ( dom h) = ( dom f) by Def33;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ( - (f . x)) by A2, Def33;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1: 8;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: <->

      redefine

      func <-> f -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( <-> f);

        

         A1: ( dom h) = ( dom f) by Def33;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ( - (f . x)) by A2, Def33;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1: 8;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: <->

      redefine

      func <-> f -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( <-> f);

        

         A1: ( dom h) = ( dom f) by Def33;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ( - (f . x)) by A2, Def33;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1: 8;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: <->

      redefine

      func <-> f -> PartFunc of X, ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( <-> f);

        

         A1: ( dom h) = ( dom f) by Def33;

        ( rng h) c= ( I_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ( - (f . x)) by A2, Def33;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1: 8;

          then y is PartFunc of ( DOMS Y), INT by A6, A5, RELSET_1: 4;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    registration

      let Y be complex-functions-membered set;

      let f be FinSequence of Y;

      cluster ( <-> f) -> FinSequence-like;

      coherence

      proof

        ( dom ( <-> f)) = ( dom f) & ex n be Nat st ( dom f) = ( Seg n) by Def33, FINSEQ_1:def 2;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    theorem :: VALUED_2:41

    ( <-> ( <-> f)) = f

    proof

      set f1 = ( <-> f);

      

       A1: ( dom f1) = ( dom f) by Def33;

      hence

       A2: ( dom ( <-> f1)) = ( dom f) by Def33;

      let x be object;

      assume

       A3: x in ( dom ( <-> f1));

      

      hence (( <-> f1) . x) = ( - (f1 . x)) by Def33

      .= ( - ( - (f . x))) by A1, A2, A3, Def33

      .= (f . x);

    end;

    theorem :: VALUED_2:42

    ( <-> f1) = ( <-> f2) implies f1 = f2

    proof

      

       A1: ( dom ( <-> f1)) = ( dom f1) by Def33;

      assume

       A2: ( <-> f1) = ( <-> f2);

      hence ( dom f1) = ( dom f2) by A1, Def33;

      let x be object;

      assume

       A3: x in ( dom f1);

      

      thus (f1 . x) = ( - ( - (f1 . x)))

      .= ( - (( <-> f1) . x)) by A1, A3, Def33

      .= ( - ( - (f2 . x))) by A2, A1, A3, Def33

      .= (f2 . x);

    end;

    definition

      let X be complex-functions-membered set;

      let Y be set;

      let f be PartFunc of X, Y;

      defpred P[ object, object] means ex a be complex-valued Function st $1 = a & $2 = (f . ( - a));

      :: VALUED_2:def34

      func f (-) -> Function means ( dom it ) = ( dom f) & for x be complex-valued Function st x in ( dom it ) holds (it . x) = (f . ( - x));

      existence

      proof

        

         A1: for x be object st x in ( dom f) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider a = x as complex-valued Function;

          take (f . ( - a)), a;

          thus thesis;

        end;

        consider F be Function such that

         A2: ( dom F) = ( dom f) and

         A3: for x be object st x in ( dom f) holds P[x, (F . x)] from CLASSES1:sch 1( A1);

        take F;

        thus ( dom F) = ( dom f) by A2;

        let x be complex-valued Function;

        assume x in ( dom F);

        then P[x, (F . x)] by A2, A3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A4: ( dom F) = ( dom f) and

         A5: for x be complex-valued Function st x in ( dom F) holds (F . x) = (f . ( - x)) and

         A6: ( dom G) = ( dom f) and

         A7: for x be complex-valued Function st x in ( dom G) holds (G . x) = (f . ( - x));

        thus ( dom F) = ( dom G) by A4, A6;

        let x be object;

        assume

         A8: x in ( dom F);

        then

        reconsider y = x as complex-valued Function by A4;

        

        thus (F . x) = (f . ( - y)) by A5, A8

        .= (G . x) by A4, A6, A7, A8;

      end;

    end

    definition

      let f be complex-functions-valued Function;

      deffunc F( object) = ((f . $1) " );

      :: VALUED_2:def35

      func </> f -> Function means

      : Def35: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) " );

      existence

      proof

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = ( dom f) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = ( dom f) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: </>

      redefine

      func </> f -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( </> f);

        

         A1: ( dom h) = ( dom f) by Def35;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) " ) by A2, Def35;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 7;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: </>

      redefine

      func </> f -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( </> f);

        

         A1: ( dom h) = ( dom f) by Def35;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) " ) by A2, Def35;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 7;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: </>

      redefine

      func </> f -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( </> f);

        

         A1: ( dom h) = ( dom f) by Def35;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) " ) by A2, Def35;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 7;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    registration

      let Y be complex-functions-membered set;

      let f be FinSequence of Y;

      cluster ( </> f) -> FinSequence-like;

      coherence

      proof

        ( dom ( </> f)) = ( dom f) & ex n be Nat st ( dom f) = ( Seg n) by Def35, FINSEQ_1:def 2;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    theorem :: VALUED_2:43

    ( </> ( </> f)) = f

    proof

      set f1 = ( </> f);

      

       A1: ( dom f1) = ( dom f) by Def35;

      hence

       A2: ( dom ( </> f1)) = ( dom f) by Def35;

      let x be object;

      assume

       A3: x in ( dom ( </> f1));

      

      hence (( </> f1) . x) = ((f1 . x) " ) by Def35

      .= (((f . x) " ) " ) by A1, A2, A3, Def35

      .= (f . x);

    end;

    definition

      let f be complex-functions-valued Function;

      deffunc F( object) = ( abs (f . $1));

      :: VALUED_2:def36

      func abs (f) -> Function means

      : Def36: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = ( abs (f . x));

      existence

      proof

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = ( dom f) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = ( dom f) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( abs f);

        

         A1: ( dom h) = ( dom f) by Def36;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ( abs (f . x)) by A2, Def36;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 11;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( abs f);

        

         A1: ( dom h) = ( dom f) by Def36;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ( abs (f . x)) by A2, Def36;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 11;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( abs f);

        

         A1: ( dom h) = ( dom f) by Def36;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ( abs (f . x)) by A2, Def36;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 11;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      :: original: abs

      redefine

      func abs (f) -> PartFunc of X, ( N_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = ( abs f);

        

         A1: ( dom h) = ( dom f) by Def36;

        ( rng h) c= ( N_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ( abs (f . x)) by A2, Def36;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 11;

          then y is PartFunc of ( DOMS Y), NAT by A6, A5, RELSET_1: 4;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    registration

      let Y be complex-functions-membered set;

      let f be FinSequence of Y;

      cluster ( abs f) -> FinSequence-like;

      coherence

      proof

        ( dom ( abs f)) = ( dom f) & ex n be Nat st ( dom f) = ( Seg n) by Def36, FINSEQ_1:def 2;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    theorem :: VALUED_2:44

    ( abs ( abs f)) = ( abs f)

    proof

      set f1 = ( abs f);

      thus

       A1: ( dom ( abs f1)) = ( dom ( abs f)) by Def36;

      let x be object;

      assume

       A2: x in ( dom ( abs f1));

      

      hence (( abs f1) . x) = ( abs (f1 . x)) by Def36

      .= ( abs ( abs (f . x))) by A1, A2, Def36

      .= (( abs f) . x) by A1, A2, Def36;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let c be Complex;

      deffunc F( object) = (c + (f . $1));

      :: VALUED_2:def37

      func f [+] c -> Function means

      : Def37: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = (c + (f . x));

      existence

      proof

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = ( dom f) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = ( dom f) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Complex;

      :: original: [+]

      redefine

      func f [+] c -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [+] c);

        

         A1: ( dom h) = ( dom f) by Def37;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) + c) by A2, Def37;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Real;

      :: original: [+]

      redefine

      func f [+] c -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [+] c);

        

         A1: ( dom h) = ( dom f) by Def37;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + c) by A2, Def37;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Rational;

      :: original: [+]

      redefine

      func f [+] c -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [+] c);

        

         A1: ( dom h) = ( dom f) by Def37;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + c) by A2, Def37;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Integer;

      :: original: [+]

      redefine

      func f [+] c -> PartFunc of X, ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [+] c);

        

         A1: ( dom h) = ( dom f) by Def37;

        ( rng h) c= ( I_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + c) by A2, Def37;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), INT by A6, A5, RELSET_1: 4;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be natural-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Nat;

      :: original: [+]

      redefine

      func f [+] c -> PartFunc of X, ( N_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [+] c);

        

         A1: ( dom h) = ( dom f) by Def37;

        ( rng h) c= ( N_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + c) by A2, Def37;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), NAT by A6, A5, RELSET_1: 4;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:45

    ((f [+] c1) [+] c2) = (f [+] (c1 + c2))

    proof

      set f1 = (f [+] c1);

      

       A1: ( dom (f1 [+] c2)) = ( dom f1) by Def37;

      ( dom f1) = ( dom f) by Def37;

      hence

       A2: ( dom (f1 [+] c2)) = ( dom (f [+] (c1 + c2))) by A1, Def37;

      let x be object;

      assume

       A3: x in ( dom (f1 [+] c2));

      

      hence ((f1 [+] c2) . x) = ((f1 . x) + c2) by Def37

      .= (((f . x) + c1) + c2) by A1, A3, Def37

      .= ((f . x) + (c1 + c2)) by Th12

      .= ((f [+] (c1 + c2)) . x) by A2, A3, Def37;

    end;

    theorem :: VALUED_2:46

    f <> {} & f is non-empty & (f [+] c1) = (f [+] c2) implies c1 = c2

    proof

      assume that

       A1: f <> {} and

       A2: f is non-empty and

       A3: (f [+] c1) = (f [+] c2);

      consider x be object such that

       A4: x in ( dom f) by A1, XBOOLE_0:def 1;

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

      then

       A5: (f . x) <> {} by A2, RELAT_1:def 9;

      ( dom f) = ( dom (f [+] c2)) by Def37;

      then

       A6: ((f [+] c2) . x) = ((f . x) + c2) by A4, Def37;

      ( dom f) = ( dom (f [+] c1)) by Def37;

      then ((f [+] c1) . x) = ((f . x) + c1) by A4, Def37;

      hence c1 = c2 by A3, A5, A6, Th7;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let c be Complex;

      :: VALUED_2:def38

      func f [-] c -> Function equals (f [+] ( - c));

      coherence ;

    end

    theorem :: VALUED_2:47

    ( dom (f [-] c)) = ( dom f) by Def37;

    theorem :: VALUED_2:48

    x in ( dom (f [-] c)) implies ((f [-] c) . x) = ((f . x) - c) by Def37;

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Complex;

      :: original: [-]

      redefine

      func f [-] c -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [-] c) = (f [+] ( - c));

        hence thesis;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Real;

      :: original: [-]

      redefine

      func f [-] c -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [-] c) = (f [+] ( - c));

        hence thesis;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Rational;

      :: original: [-]

      redefine

      func f [-] c -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [-] c) = (f [+] ( - c));

        hence thesis;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Integer;

      :: original: [-]

      redefine

      func f [-] c -> PartFunc of X, ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [-] c) = (f [+] ( - c));

        hence thesis;

      end;

    end

    theorem :: VALUED_2:49

    f <> {} & f is non-empty & (f [-] c1) = (f [-] c2) implies c1 = c2

    proof

      assume that

       A1: f <> {} and

       A2: f is non-empty and

       A3: (f [-] c1) = (f [-] c2);

      consider x be object such that

       A4: x in ( dom f) by A1, XBOOLE_0:def 1;

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

      then

       A5: (f . x) <> {} by A2, RELAT_1:def 9;

      ( dom f) = ( dom (f [-] c2)) by Def37;

      then

       A6: ((f [-] c2) . x) = ((f . x) - c2) by A4, Def37;

      ( dom f) = ( dom (f [-] c1)) by Def37;

      then ((f [-] c1) . x) = ((f . x) - c1) by A4, Def37;

      hence c1 = c2 by A3, A5, A6, Th8;

    end;

    theorem :: VALUED_2:50

    ((f [+] c1) [-] c2) = (f [+] (c1 - c2))

    proof

      set f1 = (f [+] c1);

      

       A1: ( dom (f1 [-] c2)) = ( dom f1) by Def37;

      ( dom f1) = ( dom f) by Def37;

      hence

       A2: ( dom (f1 [-] c2)) = ( dom (f [+] (c1 - c2))) by A1, Def37;

      let x be object;

      assume

       A3: x in ( dom (f1 [-] c2));

      

      hence ((f1 [-] c2) . x) = ((f1 . x) - c2) by Def37

      .= (((f . x) + c1) - c2) by A1, A3, Def37

      .= ((f . x) + (c1 - c2)) by Th12

      .= ((f [+] (c1 - c2)) . x) by A2, A3, Def37;

    end;

    theorem :: VALUED_2:51

    ((f [-] c1) [+] c2) = (f [-] (c1 - c2))

    proof

      set f1 = (f [-] c1);

      

       A1: ( dom (f1 [+] c2)) = ( dom f1) by Def37;

      ( dom f1) = ( dom f) by Def37;

      hence

       A2: ( dom (f1 [+] c2)) = ( dom (f [-] (c1 - c2))) by A1, Def37;

      let x be object;

      assume

       A3: x in ( dom (f1 [+] c2));

      

      hence ((f1 [+] c2) . x) = ((f1 . x) + c2) by Def37

      .= (((f . x) - c1) + c2) by A1, A3, Def37

      .= ((f . x) - (c1 - c2)) by Th14

      .= ((f [-] (c1 - c2)) . x) by A2, A3, Def37;

    end;

    theorem :: VALUED_2:52

    ((f [-] c1) [-] c2) = (f [-] (c1 + c2))

    proof

      set f1 = (f [-] c1);

      

       A1: ( dom (f1 [-] c2)) = ( dom f1) by Def37;

      ( dom f1) = ( dom f) by Def37;

      hence

       A2: ( dom (f1 [-] c2)) = ( dom (f [-] (c1 + c2))) by A1, Def37;

      let x be object;

      assume

       A3: x in ( dom (f1 [-] c2));

      

      hence ((f1 [-] c2) . x) = ((f1 . x) - c2) by Def37

      .= (((f . x) - c1) - c2) by A1, A3, Def37

      .= ((f . x) - (c1 + c2)) by Th15

      .= ((f [-] (c1 + c2)) . x) by A2, A3, Def37;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let c be Complex;

      deffunc F( object) = (c (#) (f . $1));

      :: VALUED_2:def39

      func f [#] c -> Function means

      : Def39: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = (c (#) (f . x));

      existence

      proof

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = ( dom f) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = ( dom f) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Complex;

      :: original: [#]

      redefine

      func f [#] c -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [#] c);

        

         A1: ( dom h) = ( dom f) by Def39;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = (c (#) (f . x)) by A2, Def39;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Real;

      :: original: [#]

      redefine

      func f [#] c -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [#] c);

        

         A1: ( dom h) = ( dom f) by Def39;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = (c (#) (f . x)) by A2, Def39;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Rational;

      :: original: [#]

      redefine

      func f [#] c -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [#] c);

        

         A1: ( dom h) = ( dom f) by Def39;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = (c (#) (f . x)) by A2, Def39;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Integer;

      :: original: [#]

      redefine

      func f [#] c -> PartFunc of X, ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [#] c);

        

         A1: ( dom h) = ( dom f) by Def39;

        ( rng h) c= ( I_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = (c (#) (f . x)) by A2, Def39;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), INT by A6, A5, RELSET_1: 4;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be natural-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Nat;

      :: original: [#]

      redefine

      func f [#] c -> PartFunc of X, ( N_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f [#] c);

        

         A1: ( dom h) = ( dom f) by Def39;

        ( rng h) c= ( N_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = (c (#) (f . x)) by A2, Def39;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          (f . x) in Y by A1, A2, PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), NAT by A6, A5, RELSET_1: 4;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:53

    ((f [#] c1) [#] c2) = (f [#] (c1 * c2))

    proof

      set f1 = (f [#] c1);

      

       A1: ( dom (f1 [#] c2)) = ( dom f1) by Def39;

      ( dom f1) = ( dom f) by Def39;

      hence

       A2: ( dom (f1 [#] c2)) = ( dom (f [#] (c1 * c2))) by A1, Def39;

      let x be object;

      assume

       A3: x in ( dom (f1 [#] c2));

      

      hence ((f1 [#] c2) . x) = ((f1 . x) (#) c2) by Def39

      .= (((f . x) (#) c1) (#) c2) by A1, A3, Def39

      .= ((f . x) (#) (c1 * c2)) by Th16

      .= ((f [#] (c1 * c2)) . x) by A2, A3, Def39;

    end;

    theorem :: VALUED_2:54

    f <> {} & f is non-empty & (for x st x in ( dom f) holds (f . x) is non-empty) & (f [#] c1) = (f [#] c2) implies c1 = c2

    proof

      assume that

       A1: f <> {} and

       A2: f is non-empty and

       A3: for x st x in ( dom f) holds (f . x) is non-empty and

       A4: (f [#] c1) = (f [#] c2);

      consider x be object such that

       A5: x in ( dom f) by A1, XBOOLE_0:def 1;

      ( dom f) = ( dom (f [#] c2)) by Def39;

      then

       A6: ((f [#] c2) . x) = ((f . x) (#) c2) by A5, Def39;

      ( dom f) = ( dom (f [#] c1)) by Def39;

      then

       A7: ((f [#] c1) . x) = ((f . x) (#) c1) by A5, Def39;

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

      then

       A8: (f . x) <> {} by A2, RELAT_1:def 9;

      (f . x) is non-empty by A3, A5;

      hence c1 = c2 by A4, A8, A7, A6, Th9;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let c be Complex;

      :: VALUED_2:def40

      func f [/] c -> Function equals (f [#] (c " ));

      coherence ;

    end

    theorem :: VALUED_2:55

    ( dom (f [/] c)) = ( dom f) by Def39;

    theorem :: VALUED_2:56

    x in ( dom (f [/] c)) implies ((f [/] c) . x) = ((c " ) (#) (f . x)) by Def39;

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Complex;

      :: original: [/]

      redefine

      func f [/] c -> PartFunc of X, ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [/] c) = (f [#] (c " ));

        hence thesis;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Real;

      :: original: [/]

      redefine

      func f [/] c -> PartFunc of X, ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [/] c) = (f [#] (c " ));

        hence thesis;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let c be Rational;

      :: original: [/]

      redefine

      func f [/] c -> PartFunc of X, ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f [/] c) = (f [#] (c " ));

        hence thesis;

      end;

    end

    theorem :: VALUED_2:57

    ((f [/] c1) [/] c2) = (f [/] (c1 * c2))

    proof

      set f1 = (f [/] c1);

      

       A1: ( dom (f1 [/] c2)) = ( dom f1) by Def39;

      ( dom f1) = ( dom f) by Def39;

      hence

       A2: ( dom (f1 [/] c2)) = ( dom (f [/] (c1 * c2))) by A1, Def39;

      let x be object;

      assume

       A3: x in ( dom (f1 [/] c2));

      

      hence ((f1 [/] c2) . x) = ((f1 . x) (#) (c2 " )) by Def39

      .= (((f . x) (#) (c1 " )) (#) (c2 " )) by A1, A3, Def39

      .= ((f . x) (#) ((c1 " ) * (c2 " ))) by Th16

      .= ((f . x) (#) ((c1 * c2) " )) by XCMPLX_1: 204

      .= ((f [/] (c1 * c2)) . x) by A2, A3, Def39;

    end;

    theorem :: VALUED_2:58

    f <> {} & f is non-empty & (for x st x in ( dom f) holds (f . x) is non-empty) & (f [/] c1) = (f [/] c2) implies c1 = c2

    proof

      assume that

       A1: f <> {} and

       A2: f is non-empty and

       A3: for x st x in ( dom f) holds (f . x) is non-empty and

       A4: (f [/] c1) = (f [/] c2);

      consider x be object such that

       A5: x in ( dom f) by A1, XBOOLE_0:def 1;

      ( dom f) = ( dom (f [/] c2)) by Def39;

      then

       A6: ((f [/] c2) . x) = ((f . x) (/) c2) by A5, Def39;

      ( dom f) = ( dom (f [/] c1)) by Def39;

      then

       A7: ((f [/] c1) . x) = ((f . x) (/) c1) by A5, Def39;

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

      then

       A8: (f . x) <> {} by A2, RELAT_1:def 9;

      (f . x) is non-empty by A3, A5;

      hence c1 = c2 by A4, A8, A7, A6, Th33;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let g be complex-valued Function;

      deffunc F( object) = ((f . $1) + (g . $1));

      :: VALUED_2:def41

      func f <+> g -> Function means

      : Def41: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) + (g . x));

      existence

      proof

        ex F be Function st ( dom F) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let g be complex-valued Function;

      :: original: <+>

      redefine

      func f <+> g -> PartFunc of (X /\ ( dom g)), ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <+> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def41;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def41;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let g be real-valued Function;

      :: original: <+>

      redefine

      func f <+> g -> PartFunc of (X /\ ( dom g)), ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <+> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def41;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def41;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let g be RAT -valued Function;

      :: original: <+>

      redefine

      func f <+> g -> PartFunc of (X /\ ( dom g)), ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <+> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def41;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def41;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      let g be INT -valued Function;

      :: original: <+>

      redefine

      func f <+> g -> PartFunc of (X /\ ( dom g)), ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <+> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def41;

        ( rng h) c= ( I_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def41;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), INT by A6, A5, RELSET_1: 4;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be natural-functions-membered set;

      let f be PartFunc of X, Y;

      let g be natural-valued Function;

      :: original: <+>

      redefine

      func f <+> g -> PartFunc of (X /\ ( dom g)), ( N_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <+> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def41;

        ( rng h) c= ( N_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def41;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), NAT by A6, A5, RELSET_1: 4;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:59

    ((f <+> g) <+> h) = (f <+> (g + h))

    proof

      set f1 = (f <+> g);

      

       A1: ( dom (g + h)) = (( dom g) /\ ( dom h)) by VALUED_1:def 1;

      

       A2: ( dom (f1 <+> h)) = (( dom f1) /\ ( dom h)) by Def41;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <+> (g + h))) = (( dom f) /\ ( dom (g + h))) by Def41;

      hence

       A3: ( dom (f1 <+> h)) = ( dom (f <+> (g + h))) by A2, A1, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f1 <+> h));

      then

       A5: x in ( dom f1) by A2, XBOOLE_0:def 4;

      

       A6: x in ( dom (g + h)) by A3, A4, XBOOLE_0:def 4;

      

      thus ((f1 <+> h) . x) = ((f1 . x) + (h . x)) by A4, Def41

      .= (((f . x) + (g . x)) + (h . x)) by A5, Def41

      .= ((f . x) + ((g . x) + (h . x))) by Th12

      .= ((f . x) + ((g + h) . x)) by A6, VALUED_1:def 1

      .= ((f <+> (g + h)) . x) by A3, A4, Def41;

    end;

    theorem :: VALUED_2:60

    ( <-> (f <+> g)) = (( <-> f) <+> ( - g))

    proof

      set f1 = (f <+> g), f2 = ( <-> f);

      

       A1: ( dom ( <-> f1)) = ( dom f1) by Def33;

      

       A2: ( dom f1) = (( dom f) /\ ( dom g)) & ( dom f2) = ( dom f) by Def33, Def41;

      ( dom ( - g)) = ( dom g) by VALUED_1: 8;

      hence

       A3: ( dom ( <-> f1)) = ( dom (f2 <+> ( - g))) by A1, A2, Def41;

      let x be object;

      assume

       A4: x in ( dom ( <-> f1));

      then

       A5: x in ( dom f2) by A1, A2, XBOOLE_0:def 4;

      

      thus (( <-> f1) . x) = ( - (f1 . x)) by A4, Def33

      .= ( - ((f . x) + (g . x))) by A1, A4, Def41

      .= (( - (f . x)) - (g . x)) by Th10

      .= (( - (f . x)) + (( - g) . x)) by VALUED_1: 8

      .= ((f2 . x) + (( - g) . x)) by A5, Def33

      .= ((f2 <+> ( - g)) . x) by A3, A4, Def41;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let g be complex-valued Function;

      :: VALUED_2:def42

      func f <-> g -> Function equals (f <+> ( - g));

      coherence ;

    end

    theorem :: VALUED_2:61

    

     Th61: ( dom (f <-> g)) = (( dom f) /\ ( dom g))

    proof

      

      thus ( dom (f <-> g)) = (( dom f) /\ ( dom ( - g))) by Def41

      .= (( dom f) /\ ( dom g)) by VALUED_1: 8;

    end;

    theorem :: VALUED_2:62

    

     Th62: x in ( dom (f <-> g)) implies ((f <-> g) . x) = ((f . x) - (g . x))

    proof

      assume x in ( dom (f <-> g));

      

      hence ((f <-> g) . x) = ((f . x) + (( - g) . x)) by Def41

      .= ((f . x) - (g . x)) by VALUED_1: 8;

    end;

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let g be complex-valued Function;

      :: original: <->

      redefine

      func f <-> g -> PartFunc of (X /\ ( dom g)), ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <-> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Th61;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Th62;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          (h . x) = ((f . x) - (g . x)) by A2, Th62;

          then ( dom y) = ( dom (f . x)) by A3, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let g be real-valued Function;

      :: original: <->

      redefine

      func f <-> g -> PartFunc of (X /\ ( dom g)), ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <-> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Th61;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Th62;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let g be RAT -valued Function;

      :: original: <->

      redefine

      func f <-> g -> PartFunc of (X /\ ( dom g)), ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <-> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Th61;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Th62;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      let g be INT -valued Function;

      :: original: <->

      redefine

      func f <-> g -> PartFunc of (X /\ ( dom g)), ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <-> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Th61;

        ( rng h) c= ( I_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Th62;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 2;

          then y is PartFunc of ( DOMS Y), INT by A6, A5, RELSET_1: 4;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:63

    (f <-> ( - g)) = (f <+> g);

    theorem :: VALUED_2:64

    ( <-> (f <-> g)) = (( <-> f) <+> g)

    proof

      set f1 = (f <-> g), f2 = ( <-> f);

      

       A1: ( dom ( <-> f1)) = ( dom f1) by Def33;

      

       A2: ( dom f1) = (( dom f) /\ ( dom g)) & ( dom f2) = ( dom f) by Def33, Th61;

      hence

       A3: ( dom ( <-> f1)) = ( dom (f2 <+> g)) by A1, Def41;

      let x be object;

      assume

       A4: x in ( dom ( <-> f1));

      then

       A5: x in ( dom f2) by A1, A2, XBOOLE_0:def 4;

      

      thus (( <-> f1) . x) = ( - (f1 . x)) by A4, Def33

      .= ( - ((f . x) - (g . x))) by A1, A4, Th62

      .= (( - (f . x)) + (g . x)) by Th11

      .= ((f2 . x) + (g . x)) by A5, Def33

      .= ((f2 <+> g) . x) by A3, A4, Def41;

    end;

    theorem :: VALUED_2:65

    ((f <+> g) <-> h) = (f <+> (g - h))

    proof

      set f1 = (f <+> g);

      

       A1: ( dom (g - h)) = (( dom g) /\ ( dom h)) by VALUED_1: 12;

      

       A2: ( dom (f1 <-> h)) = (( dom f1) /\ ( dom h)) by Th61;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <+> (g - h))) = (( dom f) /\ ( dom (g - h))) by Def41;

      hence

       A3: ( dom (f1 <-> h)) = ( dom (f <+> (g - h))) by A2, A1, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f1 <-> h));

      then

       A5: x in ( dom f1) by A2, XBOOLE_0:def 4;

      

       A6: x in ( dom (g - h)) by A3, A4, XBOOLE_0:def 4;

      

      thus ((f1 <-> h) . x) = ((f1 . x) - (h . x)) by A4, Th62

      .= (((f . x) + (g . x)) - (h . x)) by A5, Def41

      .= ((f . x) + ((g . x) - (h . x))) by Th13

      .= ((f . x) + ((g - h) . x)) by A6, VALUED_1: 13

      .= ((f <+> (g - h)) . x) by A3, A4, Def41;

    end;

    theorem :: VALUED_2:66

    ((f <-> g) <+> h) = (f <-> (g - h))

    proof

      set f1 = (f <-> g);

      

       A1: ( dom (g - h)) = (( dom g) /\ ( dom h)) by VALUED_1: 12;

      

       A2: ( dom (f1 <+> h)) = (( dom f1) /\ ( dom h)) by Def41;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <-> (g - h))) = (( dom f) /\ ( dom (g - h))) by Th61;

      hence

       A3: ( dom (f1 <+> h)) = ( dom (f <-> (g - h))) by A2, A1, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f1 <+> h));

      then

       A5: x in ( dom f1) by A2, XBOOLE_0:def 4;

      

       A6: x in ( dom (g - h)) by A3, A4, XBOOLE_0:def 4;

      

      thus ((f1 <+> h) . x) = ((f1 . x) + (h . x)) by A4, Def41

      .= (((f . x) - (g . x)) + (h . x)) by A5, Th62

      .= ((f . x) - ((g . x) - (h . x))) by Th14

      .= ((f . x) - ((g - h) . x)) by A6, VALUED_1: 13

      .= ((f <-> (g - h)) . x) by A3, A4, Th62;

    end;

    theorem :: VALUED_2:67

    ((f <-> g) <-> h) = (f <-> (g + h))

    proof

      set f1 = (f <-> g);

      

       A1: ( dom (g + h)) = (( dom g) /\ ( dom h)) by VALUED_1:def 1;

      

       A2: ( dom (f1 <-> h)) = (( dom f1) /\ ( dom h)) by Th61;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <-> (g + h))) = (( dom f) /\ ( dom (g + h))) by Th61;

      hence

       A3: ( dom (f1 <-> h)) = ( dom (f <-> (g + h))) by A2, A1, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f1 <-> h));

      then

       A5: x in ( dom f1) by A2, XBOOLE_0:def 4;

      

       A6: x in ( dom (g + h)) by A3, A4, XBOOLE_0:def 4;

      

      thus ((f1 <-> h) . x) = ((f1 . x) - (h . x)) by A4, Th62

      .= (((f . x) - (g . x)) - (h . x)) by A5, Th62

      .= ((f . x) - ((g . x) + (h . x))) by Th15

      .= ((f . x) - ((g + h) . x)) by A6, VALUED_1:def 1

      .= ((f <-> (g + h)) . x) by A3, A4, Th62;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let g be complex-valued Function;

      deffunc F( object) = ((f . $1) (#) (g . $1));

      :: VALUED_2:def43

      func f <#> g -> Function means

      : Def43: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) (#) (g . x));

      existence

      proof

        ex F be Function st ( dom F) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let g be complex-valued Function;

      :: original: <#>

      redefine

      func f <#> g -> PartFunc of (X /\ ( dom g)), ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <#> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def43;

        ( rng h) c= ( C_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def43;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), COMPLEX by A6, A5, RELSET_1: 4;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let g be real-valued Function;

      :: original: <#>

      redefine

      func f <#> g -> PartFunc of (X /\ ( dom g)), ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <#> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def43;

        ( rng h) c= ( R_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def43;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), REAL by A6, A5, RELSET_1: 4;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let g be RAT -valued Function;

      :: original: <#>

      redefine

      func f <#> g -> PartFunc of (X /\ ( dom g)), ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <#> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def43;

        ( rng h) c= ( Q_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def43;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), RAT by A6, A5, RELSET_1: 4;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be integer-functions-membered set;

      let f be PartFunc of X, Y;

      let g be INT -valued Function;

      :: original: <#>

      redefine

      func f <#> g -> PartFunc of (X /\ ( dom g)), ( I_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <#> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def43;

        ( rng h) c= ( I_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def43;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), INT by A6, A5, RELSET_1: 4;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X;

      let Y be natural-functions-membered set;

      let f be PartFunc of X, Y;

      let g be natural-valued Function;

      :: original: <#>

      redefine

      func f <#> g -> PartFunc of (X /\ ( dom g)), ( N_PFuncs ( DOMS Y)) ;

      coherence

      proof

        set h = (f <#> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def43;

        ( rng h) c= ( N_PFuncs ( DOMS Y))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def43;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y;

          then

           A6: ( dom (f . x)) c= ( DOMS Y) by ZFMISC_1: 74;

          ( dom y) = ( dom (f . x)) by A3, A4, VALUED_1:def 5;

          then y is PartFunc of ( DOMS Y), NAT by A6, A5, RELSET_1: 4;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:68

    (f <#> ( - g)) = (( <-> f) <#> g)

    proof

      set f1 = ( <-> f);

      

       A1: ( dom f1) = ( dom f) & ( dom (f <#> ( - g))) = (( dom f) /\ ( dom ( - g))) by Def33, Def43;

      ( dom (f1 <#> g)) = (( dom f1) /\ ( dom g)) by Def43;

      hence

       A2: ( dom (f <#> ( - g))) = ( dom (f1 <#> g)) by A1, VALUED_1: 8;

      let x be object;

      assume

       A3: x in ( dom (f <#> ( - g)));

      then

       A4: x in ( dom f1) by A1, XBOOLE_0:def 4;

      

      thus ((f <#> ( - g)) . x) = ((f . x) (#) (( - g) . x)) by A3, Def43

      .= ((f . x) (#) ( - (g . x))) by VALUED_1: 8

      .= (( - (f . x)) (#) (g . x)) by Th22

      .= ((f1 . x) (#) (g . x)) by A4, Def33

      .= ((f1 <#> g) . x) by A2, A3, Def43;

    end;

    theorem :: VALUED_2:69

    (f <#> ( - g)) = ( <-> (f <#> g))

    proof

      set f1 = (f <#> g);

      

       A1: ( dom ( <-> f1)) = ( dom f1) by Def33;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <#> ( - g))) = (( dom f) /\ ( dom ( - g))) by Def43;

      hence

       A2: ( dom (f <#> ( - g))) = ( dom ( <-> f1)) by A1, VALUED_1: 8;

      let x be object;

      assume

       A3: x in ( dom (f <#> ( - g)));

      

      hence ((f <#> ( - g)) . x) = ((f . x) (#) (( - g) . x)) by Def43

      .= ((f . x) (#) ( - (g . x))) by VALUED_1: 8

      .= ( - ((f . x) (#) (g . x))) by Th24

      .= ( - (f1 . x)) by A1, A2, A3, Def43

      .= (( <-> f1) . x) by A2, A3, Def33;

    end;

    theorem :: VALUED_2:70

    ((f <#> g) <#> h) = (f <#> (g (#) h))

    proof

      set f1 = (f <#> g);

      

       A1: ( dom (g (#) h)) = (( dom g) /\ ( dom h)) by VALUED_1:def 4;

      

       A2: ( dom (f1 <#> h)) = (( dom f1) /\ ( dom h)) by Def43;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <#> (g (#) h))) = (( dom f) /\ ( dom (g (#) h))) by Def43;

      hence

       A3: ( dom (f1 <#> h)) = ( dom (f <#> (g (#) h))) by A2, A1, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f1 <#> h));

      then

       A5: x in ( dom f1) by A2, XBOOLE_0:def 4;

      

       A6: x in ( dom (g (#) h)) by A3, A4, XBOOLE_0:def 4;

      

      thus ((f1 <#> h) . x) = ((f1 . x) (#) (h . x)) by A4, Def43

      .= (((f . x) (#) (g . x)) (#) (h . x)) by A5, Def43

      .= ((f . x) (#) ((g . x) * (h . x))) by Th16

      .= ((f . x) (#) ((g (#) h) . x)) by A6, VALUED_1:def 4

      .= ((f <#> (g (#) h)) . x) by A3, A4, Def43;

    end;

    definition

      let Y be complex-functions-membered set;

      let f be Y -valued Function;

      let g be complex-valued Function;

      :: VALUED_2:def44

      func f </> g -> Function equals (f <#> (g " ));

      coherence ;

    end

    theorem :: VALUED_2:71

    

     Th71: ( dom (f </> g)) = (( dom f) /\ ( dom g))

    proof

      

      thus ( dom (f </> g)) = (( dom f) /\ ( dom (g " ))) by Def43

      .= (( dom f) /\ ( dom g)) by VALUED_1:def 7;

    end;

    theorem :: VALUED_2:72

    

     Th72: x in ( dom (f </> g)) implies ((f </> g) . x) = ((f . x) (/) (g . x))

    proof

      assume x in ( dom (f </> g));

      

      hence ((f </> g) . x) = ((f . x) (#) ((g " ) . x)) by Def43

      .= ((f . x) (/) (g . x)) by VALUED_1: 10;

    end;

    definition

      let X;

      let Y be complex-functions-membered set;

      let f be PartFunc of X, Y;

      let g be complex-valued Function;

      :: original: </>

      redefine

      func f </> g -> PartFunc of (X /\ ( dom g)), ( C_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f </> g) = (f <#> (g " ));

        hence thesis by VALUED_1:def 7;

      end;

    end

    definition

      let X;

      let Y be real-functions-membered set;

      let f be PartFunc of X, Y;

      let g be real-valued Function;

      :: original: </>

      redefine

      func f </> g -> PartFunc of (X /\ ( dom g)), ( R_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f </> g) = (f <#> (g " ));

        hence thesis by VALUED_1:def 7;

      end;

    end

    definition

      let X;

      let Y be rational-functions-membered set;

      let f be PartFunc of X, Y;

      let g be RAT -valued Function;

      :: original: </>

      redefine

      func f </> g -> PartFunc of (X /\ ( dom g)), ( Q_PFuncs ( DOMS Y)) ;

      coherence

      proof

        (f </> g) = (f <#> (g " ));

        hence thesis by VALUED_1:def 7;

      end;

    end

    theorem :: VALUED_2:73

    ((f <#> g) </> h) = (f <#> (g /" h))

    proof

      set f1 = (f <#> g);

      

       A1: ( dom (g /" h)) = (( dom g) /\ ( dom h)) by VALUED_1: 16;

      

       A2: ( dom (f1 </> h)) = (( dom f1) /\ ( dom h)) by Th71;

      ( dom f1) = (( dom f) /\ ( dom g)) & ( dom (f <#> (g /" h))) = (( dom f) /\ ( dom (g /" h))) by Def43;

      hence

       A3: ( dom (f1 </> h)) = ( dom (f <#> (g /" h))) by A2, A1, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f1 </> h));

      then

       A5: x in ( dom f1) by A2, XBOOLE_0:def 4;

      

      thus ((f1 </> h) . x) = ((f1 . x) (/) (h . x)) by A4, Th72

      .= (((f . x) (#) (g . x)) (/) (h . x)) by A5, Def43

      .= ((f . x) (#) ((g . x) / (h . x))) by Th16

      .= ((f . x) (#) ((g /" h) . x)) by VALUED_1: 17

      .= ((f <#> (g /" h)) . x) by A3, A4, Def43;

    end;

    definition

      let Y1,Y2 be complex-functions-membered set;

      let f be Y1 -valued Function;

      let g be Y2 -valued Function;

      deffunc F( object) = ((f . $1) + (g . $1));

      :: VALUED_2:def45

      func f <++> g -> Function means

      : Def45: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) + (g . x));

      existence

      proof

        ex F be Function st ( dom F) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be complex-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <++>

      redefine

      func f <++> g -> PartFunc of (X1 /\ X2), ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <++> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def45;

        ( rng h) c= ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def45;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 1;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), COMPLEX by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be real-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <++>

      redefine

      func f <++> g -> PartFunc of (X1 /\ X2), ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <++> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def45;

        ( rng h) c= ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def45;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 1;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), REAL by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be rational-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <++>

      redefine

      func f <++> g -> PartFunc of (X1 /\ X2), ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <++> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def45;

        ( rng h) c= ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def45;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 1;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), RAT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be integer-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <++>

      redefine

      func f <++> g -> PartFunc of (X1 /\ X2), ( I_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <++> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def45;

        ( rng h) c= ( I_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def45;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 1;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), INT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be natural-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <++>

      redefine

      func f <++> g -> PartFunc of (X1 /\ X2), ( N_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <++> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def45;

        ( rng h) c= ( N_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) + (g . x)) by A2, Def45;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 1;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), NAT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:74

    (f1 <++> f2) = (f2 <++> f1)

    proof

      ( dom (f1 <++> f2)) = (( dom f1) /\ ( dom f2)) by Def45;

      hence

       A1: ( dom (f1 <++> f2)) = ( dom (f2 <++> f1)) by Def45;

      let x be object;

      assume

       A2: x in ( dom (f1 <++> f2));

      

      hence ((f1 <++> f2) . x) = ((f1 . x) + (f2 . x)) by Def45

      .= ((f2 <++> f1) . x) by A1, A2, Def45;

    end;

    theorem :: VALUED_2:75

    ((f <++> f1) <++> f2) = (f <++> (f1 <++> f2))

    proof

      set f3 = (f <++> f1), f4 = (f1 <++> f2);

      

       A1: ( dom (f3 <++> f2)) = (( dom f3) /\ ( dom f2)) by Def45;

      

       A2: ( dom (f <++> f4)) = (( dom f) /\ ( dom f4)) by Def45;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def45;

      hence

       A3: ( dom (f3 <++> f2)) = ( dom (f <++> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <++> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <++> f2) . x) = ((f3 . x) + (f2 . x)) by A4, Def45

      .= (((f . x) + (f1 . x)) + (f2 . x)) by A6, Def45

      .= ((f . x) + ((f1 . x) + (f2 . x))) by RFUNCT_1: 8

      .= ((f . x) + (f4 . x)) by A5, Def45

      .= ((f <++> f4) . x) by A3, A4, Def45;

    end;

    theorem :: VALUED_2:76

    ( <-> (f1 <++> f2)) = (( <-> f1) <++> ( <-> f2))

    proof

      set f3 = (f1 <++> f2), f4 = ( <-> f1), f5 = ( <-> f2);

      

       A1: ( dom (f1 <++> f2)) = (( dom f1) /\ ( dom f2)) by Def45;

      

       A2: ( dom ( <-> f2)) = ( dom f2) by Def33;

      

       A3: ( dom ( <-> f3)) = ( dom f3) by Def33;

      

       A4: ( dom ( <-> f1)) = ( dom f1) by Def33;

      hence

       A5: ( dom ( <-> f3)) = ( dom (f4 <++> f5)) by A1, A2, A3, Def45;

      let x be object;

      assume

       A6: x in ( dom ( <-> f3));

      then

       A7: x in ( dom f4) by A1, A4, A3, XBOOLE_0:def 4;

      

       A8: x in ( dom f5) by A1, A2, A3, A6, XBOOLE_0:def 4;

      

      thus (( <-> f3) . x) = ( - (f3 . x)) by A6, Def33

      .= ( - ((f1 . x) + (f2 . x))) by A3, A6, Def45

      .= (( - (f1 . x)) - (f2 . x)) by Th17

      .= ((f4 . x) + ( - (f2 . x))) by A7, Def33

      .= ((f4 . x) + (f5 . x)) by A8, Def33

      .= ((f4 <++> f5) . x) by A5, A6, Def45;

    end;

    definition

      let Y1,Y2 be complex-functions-membered set;

      let f be Y1 -valued Function;

      let g be Y2 -valued Function;

      deffunc F( object) = ((f . $1) - (g . $1));

      :: VALUED_2:def46

      func f <--> g -> Function means

      : Def46: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) - (g . x));

      existence

      proof

        ex F be Function st ( dom F) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be complex-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <-->

      redefine

      func f <--> g -> PartFunc of (X1 /\ X2), ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <--> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def46;

        ( rng h) c= ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Def46;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 12;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), COMPLEX by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be real-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <-->

      redefine

      func f <--> g -> PartFunc of (X1 /\ X2), ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <--> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def46;

        ( rng h) c= ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Def46;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 12;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), REAL by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be rational-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <-->

      redefine

      func f <--> g -> PartFunc of (X1 /\ X2), ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <--> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def46;

        ( rng h) c= ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Def46;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 12;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), RAT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be integer-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <-->

      redefine

      func f <--> g -> PartFunc of (X1 /\ X2), ( I_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <--> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def46;

        ( rng h) c= ( I_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) - (g . x)) by A2, Def46;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 12;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), INT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:77

    (f1 <--> f2) = ( <-> (f2 <--> f1))

    proof

      set f = (f2 <--> f1);

      

       A1: ( dom (f1 <--> f2)) = (( dom f1) /\ ( dom f2)) & ( dom (f2 <--> f1)) = (( dom f2) /\ ( dom f1)) by Def46;

      hence

       A2: ( dom (f1 <--> f2)) = ( dom ( <-> f)) by Def33;

      let x be object;

      assume

       A3: x in ( dom (f1 <--> f2));

      

      hence ((f1 <--> f2) . x) = ((f1 . x) - (f2 . x)) by Def46

      .= ( - ((f2 . x) - (f1 . x))) by Th18

      .= ( - (f . x)) by A1, A3, Def46

      .= (( <-> f) . x) by A2, A3, Def33;

    end;

    theorem :: VALUED_2:78

    ( <-> (f1 <--> f2)) = (( <-> f1) <++> f2)

    proof

      set f3 = (f1 <--> f2), f4 = ( <-> f1);

      

       A1: ( dom ( <-> f3)) = ( dom f3) by Def33;

      

       A2: ( dom (f1 <--> f2)) = (( dom f1) /\ ( dom f2)) & ( dom ( <-> f1)) = ( dom f1) by Def33, Def46;

      hence

       A3: ( dom ( <-> f3)) = ( dom (f4 <++> f2)) by A1, Def45;

      let x be object;

      assume

       A4: x in ( dom ( <-> f3));

      then

       A5: x in ( dom f4) by A2, A1, XBOOLE_0:def 4;

      

      thus (( <-> f3) . x) = ( - (f3 . x)) by A4, Def33

      .= ( - ((f1 . x) - (f2 . x))) by A1, A4, Def46

      .= (( - (f1 . x)) - ( - (f2 . x))) by Th17

      .= ((f4 . x) + (f2 . x)) by A5, Def33

      .= ((f4 <++> f2) . x) by A3, A4, Def45;

    end;

    theorem :: VALUED_2:79

    ((f <++> f1) <--> f2) = (f <++> (f1 <--> f2))

    proof

      set f3 = (f <++> f1), f4 = (f1 <--> f2);

      

       A1: ( dom (f3 <--> f2)) = (( dom f3) /\ ( dom f2)) by Def46;

      

       A2: ( dom (f <++> f4)) = (( dom f) /\ ( dom f4)) by Def45;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def45, Def46;

      hence

       A3: ( dom (f3 <--> f2)) = ( dom (f <++> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <--> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <--> f2) . x) = ((f3 . x) - (f2 . x)) by A4, Def46

      .= (((f . x) + (f1 . x)) - (f2 . x)) by A6, Def45

      .= ((f . x) + ((f1 . x) - (f2 . x))) by RFUNCT_1: 8

      .= ((f . x) + (f4 . x)) by A5, Def46

      .= ((f <++> f4) . x) by A3, A4, Def45;

    end;

    theorem :: VALUED_2:80

    ((f <--> f1) <++> f2) = (f <--> (f1 <--> f2))

    proof

      set f3 = (f <--> f1), f4 = (f1 <--> f2);

      

       A1: ( dom (f3 <++> f2)) = (( dom f3) /\ ( dom f2)) by Def45;

      

       A2: ( dom (f <--> f4)) = (( dom f) /\ ( dom f4)) by Def46;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def46;

      hence

       A3: ( dom (f3 <++> f2)) = ( dom (f <--> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <++> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <++> f2) . x) = ((f3 . x) + (f2 . x)) by A4, Def45

      .= (((f . x) - (f1 . x)) + (f2 . x)) by A6, Def46

      .= ((f . x) - ((f1 . x) - (f2 . x))) by RFUNCT_1: 22

      .= ((f . x) - (f4 . x)) by A5, Def46

      .= ((f <--> f4) . x) by A3, A4, Def46;

    end;

    theorem :: VALUED_2:81

    ((f <--> f1) <--> f2) = (f <--> (f1 <++> f2))

    proof

      set f3 = (f <--> f1), f4 = (f1 <++> f2);

      

       A1: ( dom (f3 <--> f2)) = (( dom f3) /\ ( dom f2)) by Def46;

      

       A2: ( dom (f <--> f4)) = (( dom f) /\ ( dom f4)) by Def46;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def45, Def46;

      hence

       A3: ( dom (f3 <--> f2)) = ( dom (f <--> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <--> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <--> f2) . x) = ((f3 . x) - (f2 . x)) by A4, Def46

      .= (((f . x) - (f1 . x)) - (f2 . x)) by A6, Def46

      .= ((f . x) - ((f1 . x) + (f2 . x))) by RFUNCT_1: 20

      .= ((f . x) - (f4 . x)) by A5, Def45

      .= ((f <--> f4) . x) by A3, A4, Def46;

    end;

    theorem :: VALUED_2:82

    ((f <--> f1) <--> f2) = ((f <--> f2) <--> f1)

    proof

      set f3 = (f <--> f1), f4 = (f <--> f2);

      

       A1: ( dom (f3 <--> f2)) = (( dom f3) /\ ( dom f2)) by Def46;

      

       A2: ( dom (f4 <--> f1)) = (( dom f4) /\ ( dom f1)) by Def46;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f) /\ ( dom f2)) by Def46;

      hence

       A3: ( dom (f3 <--> f2)) = ( dom (f4 <--> f1)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <--> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <--> f2) . x) = ((f3 . x) - (f2 . x)) by A4, Def46

      .= (((f . x) - (f1 . x)) - (f2 . x)) by A6, Def46

      .= (((f . x) - (f2 . x)) - (f1 . x)) by RFUNCT_1: 23

      .= ((f4 . x) - (f1 . x)) by A5, Def46

      .= ((f4 <--> f1) . x) by A3, A4, Def46;

    end;

    definition

      let Y1,Y2 be complex-functions-membered set;

      let f be Y1 -valued Function;

      let g be Y2 -valued Function;

      deffunc F( object) = ((f . $1) (#) (g . $1));

      :: VALUED_2:def47

      func f <##> g -> Function means

      : Def47: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) (#) (g . x));

      existence

      proof

        ex F be Function st ( dom F) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be complex-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <##>

      redefine

      func f <##> g -> PartFunc of (X1 /\ X2), ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <##> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def47;

        ( rng h) c= ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def47;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 4;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), COMPLEX by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be real-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <##>

      redefine

      func f <##> g -> PartFunc of (X1 /\ X2), ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <##> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def47;

        ( rng h) c= ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def47;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 4;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), REAL by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be rational-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <##>

      redefine

      func f <##> g -> PartFunc of (X1 /\ X2), ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <##> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def47;

        ( rng h) c= ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def47;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 4;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), RAT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be integer-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <##>

      redefine

      func f <##> g -> PartFunc of (X1 /\ X2), ( I_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <##> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def47;

        ( rng h) c= ( I_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def47;

          

           A5: ( rng y) c= INT by A3, A4, INT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 4;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), INT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def16;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be natural-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <##>

      redefine

      func f <##> g -> PartFunc of (X1 /\ X2), ( N_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <##> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def47;

        ( rng h) c= ( N_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) (#) (g . x)) by A2, Def47;

          

           A5: ( rng y) c= NAT by A3, A4, ORDINAL1:def 12;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1:def 4;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), NAT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def18;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:83

    

     Th83: (f1 <##> f2) = (f2 <##> f1)

    proof

      ( dom (f1 <##> f2)) = (( dom f1) /\ ( dom f2)) by Def47;

      hence

       A1: ( dom (f1 <##> f2)) = ( dom (f2 <##> f1)) by Def47;

      let x be object;

      assume

       A2: x in ( dom (f1 <##> f2));

      

      hence ((f1 <##> f2) . x) = ((f1 . x) (#) (f2 . x)) by Def47

      .= ((f2 <##> f1) . x) by A1, A2, Def47;

    end;

    theorem :: VALUED_2:84

    ((f <##> f1) <##> f2) = (f <##> (f1 <##> f2))

    proof

      set f3 = (f <##> f1), f4 = (f1 <##> f2);

      

       A1: ( dom (f3 <##> f2)) = (( dom f3) /\ ( dom f2)) by Def47;

      

       A2: ( dom (f <##> f4)) = (( dom f) /\ ( dom f4)) by Def47;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def47;

      hence

       A3: ( dom (f3 <##> f2)) = ( dom (f <##> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <##> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <##> f2) . x) = ((f3 . x) (#) (f2 . x)) by A4, Def47

      .= (((f . x) (#) (f1 . x)) (#) (f2 . x)) by A6, Def47

      .= ((f . x) (#) ((f1 . x) (#) (f2 . x))) by RFUNCT_1: 9

      .= ((f . x) (#) (f4 . x)) by A5, Def47

      .= ((f <##> f4) . x) by A3, A4, Def47;

    end;

    theorem :: VALUED_2:85

    (( <-> f1) <##> f2) = ( <-> (f1 <##> f2))

    proof

      set f3 = (f1 <##> f2), f4 = ( <-> f1);

      

       A1: ( dom f3) = (( dom f1) /\ ( dom f2)) & ( dom f4) = ( dom f1) by Def33, Def47;

      ( dom (f4 <##> f2)) = (( dom f4) /\ ( dom f2)) by Def47;

      hence

       A2: ( dom (f4 <##> f2)) = ( dom ( <-> f3)) by A1, Def33;

      let x be object;

      assume

       A3: x in ( dom (f4 <##> f2));

      then

       A4: x in ( dom f3) by A1, Def47;

      then

       A5: x in ( dom ( <-> f1)) by A1, XBOOLE_0:def 4;

      

      thus ((f4 <##> f2) . x) = ((f4 . x) (#) (f2 . x)) by A3, Def47

      .= (( - (f1 . x)) (#) (f2 . x)) by A5, Def33

      .= ( - ((f1 . x) (#) (f2 . x))) by Th25

      .= ( - (f3 . x)) by A4, Def47

      .= (( <-> f3) . x) by A2, A3, Def33;

    end;

    theorem :: VALUED_2:86

    (f1 <##> ( <-> f2)) = ( <-> (f1 <##> f2))

    proof

      set f3 = (f1 <##> f2), f4 = ( <-> f2);

      

       A1: ( dom f3) = (( dom f1) /\ ( dom f2)) & ( dom f4) = ( dom f2) by Def33, Def47;

      ( dom (f1 <##> f4)) = (( dom f1) /\ ( dom f4)) by Def47;

      hence

       A2: ( dom (f1 <##> f4)) = ( dom ( <-> f3)) by A1, Def33;

      let x be object;

      assume

       A3: x in ( dom (f1 <##> f4));

      then

       A4: x in ( dom f3) by A1, Def47;

      then

       A5: x in ( dom ( <-> f2)) by A1, XBOOLE_0:def 4;

      

      thus ((f1 <##> f4) . x) = ((f1 . x) (#) (f4 . x)) by A3, Def47

      .= ((f1 . x) (#) ( - (f2 . x))) by A5, Def33

      .= ( - ((f1 . x) (#) (f2 . x))) by Th25

      .= ( - (f3 . x)) by A4, Def47

      .= (( <-> f3) . x) by A2, A3, Def33;

    end;

    theorem :: VALUED_2:87

    

     Th87: (f <##> (f1 <++> f2)) = ((f <##> f1) <++> (f <##> f2))

    proof

      set f3 = (f <##> f1), f4 = (f <##> f2), f5 = (f1 <++> f2);

      

       A1: ( dom (f <##> f5)) = (( dom f) /\ ( dom f5)) by Def47;

      

       A2: ( dom f5) = (( dom f1) /\ ( dom f2)) by Def45;

      

       A3: ( dom (f3 <++> f4)) = (( dom f3) /\ ( dom f4)) by Def45;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f) /\ ( dom f2)) by Def47;

      hence

       A4: ( dom (f <##> f5)) = ( dom (f3 <++> f4)) by A1, A3, A2, Lm1;

      let x be object;

      assume

       A5: x in ( dom (f <##> f5));

      then

       A6: x in ( dom f3) by A3, A4, XBOOLE_0:def 4;

      

       A7: x in ( dom f5) by A1, A5, XBOOLE_0:def 4;

      

       A8: x in ( dom f4) by A3, A4, A5, XBOOLE_0:def 4;

      

      thus ((f <##> f5) . x) = ((f . x) (#) (f5 . x)) by A5, Def47

      .= ((f . x) (#) ((f1 . x) + (f2 . x))) by A7, Def45

      .= (((f . x) (#) (f1 . x)) + ((f . x) (#) (f2 . x))) by RFUNCT_1: 10

      .= ((f3 . x) + ((f . x) (#) (f2 . x))) by A6, Def47

      .= ((f3 . x) + (f4 . x)) by A8, Def47

      .= ((f3 <++> f4) . x) by A4, A5, Def45;

    end;

    theorem :: VALUED_2:88

    ((f1 <++> f2) <##> f) = ((f1 <##> f) <++> (f2 <##> f))

    proof

      set f3 = (f1 <##> f), f4 = (f2 <##> f), f5 = (f1 <++> f2);

      

       A1: (f1 <##> f) = (f <##> f1) & (f2 <##> f) = (f <##> f2) by Th83;

      

      thus (f5 <##> f) = (f <##> f5) by Th83

      .= (f3 <++> f4) by A1, Th87;

    end;

    theorem :: VALUED_2:89

    

     Th89: (f <##> (f1 <--> f2)) = ((f <##> f1) <--> (f <##> f2))

    proof

      set f3 = (f <##> f1), f4 = (f <##> f2), f5 = (f1 <--> f2);

      

       A1: ( dom (f <##> f5)) = (( dom f) /\ ( dom f5)) by Def47;

      

       A2: ( dom f5) = (( dom f1) /\ ( dom f2)) by Def46;

      

       A3: ( dom (f3 <--> f4)) = (( dom f3) /\ ( dom f4)) by Def46;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f) /\ ( dom f2)) by Def47;

      hence

       A4: ( dom (f <##> f5)) = ( dom (f3 <--> f4)) by A1, A3, A2, Lm1;

      let x be object;

      assume

       A5: x in ( dom (f <##> f5));

      then

       A6: x in ( dom f3) by A3, A4, XBOOLE_0:def 4;

      

       A7: x in ( dom f5) by A1, A5, XBOOLE_0:def 4;

      

       A8: x in ( dom f4) by A3, A4, A5, XBOOLE_0:def 4;

      

      thus ((f <##> f5) . x) = ((f . x) (#) (f5 . x)) by A5, Def47

      .= ((f . x) (#) ((f1 . x) - (f2 . x))) by A7, Def46

      .= (((f . x) (#) (f1 . x)) - ((f . x) (#) (f2 . x))) by RFUNCT_1: 15

      .= ((f3 . x) - ((f . x) (#) (f2 . x))) by A6, Def47

      .= ((f3 . x) - (f4 . x)) by A8, Def47

      .= ((f3 <--> f4) . x) by A4, A5, Def46;

    end;

    theorem :: VALUED_2:90

    ((f1 <--> f2) <##> f) = ((f1 <##> f) <--> (f2 <##> f))

    proof

      set f3 = (f1 <##> f), f4 = (f2 <##> f), f5 = (f1 <--> f2);

      

       A1: (f1 <##> f) = (f <##> f1) & (f2 <##> f) = (f <##> f2) by Th83;

      

      thus (f5 <##> f) = (f <##> f5) by Th83

      .= (f3 <--> f4) by A1, Th89;

    end;

    definition

      let Y1,Y2 be complex-functions-membered set;

      let f be Y1 -valued Function;

      let g be Y2 -valued Function;

      deffunc F( object) = ((f . $1) /" (g . $1));

      :: VALUED_2:def48

      func f <//> g -> Function means

      : Def48: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = ((f . x) /" (g . x));

      existence

      proof

        ex F be Function st ( dom F) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (F . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function such that

         A1: ( dom F) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom F) holds (F . x) = F(x) and

         A3: ( dom G) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom G) holds (G . x) = F(x);

        thus ( dom F) = ( dom G) by A1, A3;

        let x be object;

        assume

         A5: x in ( dom F);

        

        hence (F . x) = F(x) by A2

        .= (G . x) by A1, A3, A4, A5;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be complex-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <//>

      redefine

      func f <//> g -> PartFunc of (X1 /\ X2), ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <//> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def48;

        ( rng h) c= ( C_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          

           A4: (h . x) = ((f . x) /" (g . x)) by A2, Def48;

          then

          reconsider y as Function by A3;

          

           A5: ( rng y) c= COMPLEX by A3, A4, XCMPLX_0:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 16;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), COMPLEX by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def8;

        end;

        hence thesis by A1, RELSET_1: 4, XBOOLE_1: 27;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be real-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <//>

      redefine

      func f <//> g -> PartFunc of (X1 /\ X2), ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <//> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def48;

        ( rng h) c= ( R_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) /" (g . x)) by A2, Def48;

          

           A5: ( rng y) c= REAL by A3, A4, XREAL_0:def 1;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 16;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), REAL by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def12;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    definition

      let X1,X2 be set;

      let Y1,Y2 be rational-functions-membered set;

      let f be PartFunc of X1, Y1;

      let g be PartFunc of X2, Y2;

      :: original: <//>

      redefine

      func f <//> g -> PartFunc of (X1 /\ X2), ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2))) ;

      coherence

      proof

        set h = (f <//> g);

        

         A1: ( dom h) = (( dom f) /\ ( dom g)) by Def48;

        ( rng h) c= ( Q_PFuncs (( DOMS Y1) /\ ( DOMS Y2)))

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A2: x in ( dom h) and

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

          reconsider y as Function by A3;

          

           A4: (h . x) = ((f . x) /" (g . x)) by A2, Def48;

          

           A5: ( rng y) c= RAT by A3, A4, RAT_1:def 2;

          x in ( dom g) by A1, A2, XBOOLE_0:def 4;

          then (g . x) in Y2 by PARTFUN1: 4;

          then ( dom (g . x)) in the set of all ( dom m) where m be Element of Y2;

          then

           A6: ( dom (g . x)) c= ( DOMS Y2) by ZFMISC_1: 74;

          x in ( dom f) by A1, A2, XBOOLE_0:def 4;

          then (f . x) in Y1 by PARTFUN1: 4;

          then ( dom (f . x)) in the set of all ( dom m) where m be Element of Y1;

          then

           A7: ( dom (f . x)) c= ( DOMS Y1) by ZFMISC_1: 74;

          ( dom y) = (( dom (f . x)) /\ ( dom (g . x))) by A3, A4, VALUED_1: 16;

          then y is PartFunc of (( DOMS Y1) /\ ( DOMS Y2)), RAT by A7, A6, A5, RELSET_1: 4, XBOOLE_1: 27;

          hence thesis by Def14;

        end;

        hence thesis by A1, RELSET_1: 4;

      end;

    end

    theorem :: VALUED_2:91

    (( <-> f1) <//> f2) = ( <-> (f1 <//> f2))

    proof

      set f3 = (f1 <//> f2), f4 = ( <-> f1);

      

       A1: ( dom f3) = (( dom f1) /\ ( dom f2)) & ( dom f4) = ( dom f1) by Def33, Def48;

      ( dom (f4 <//> f2)) = (( dom f4) /\ ( dom f2)) by Def48;

      hence

       A2: ( dom (f4 <//> f2)) = ( dom ( <-> f3)) by A1, Def33;

      let x be object;

      assume

       A3: x in ( dom (f4 <//> f2));

      then

       A4: x in ( dom f3) by A1, Def48;

      then

       A5: x in ( dom ( <-> f1)) by A1, XBOOLE_0:def 4;

      

      thus ((f4 <//> f2) . x) = ((f4 . x) /" (f2 . x)) by A3, Def48

      .= (( - (f1 . x)) /" (f2 . x)) by A5, Def33

      .= ( - ((f1 . x) /" (f2 . x))) by Th25

      .= ( - (f3 . x)) by A4, Def48

      .= (( <-> f3) . x) by A2, A3, Def33;

    end;

    theorem :: VALUED_2:92

    (f1 <//> ( <-> f2)) = ( <-> (f1 <//> f2))

    proof

      set f3 = (f1 <//> f2), f4 = ( <-> f2);

      

       A1: ( dom f3) = (( dom f1) /\ ( dom f2)) & ( dom f4) = ( dom f2) by Def33, Def48;

      ( dom (f1 <//> f4)) = (( dom f1) /\ ( dom f4)) by Def48;

      hence

       A2: ( dom (f1 <//> f4)) = ( dom ( <-> f3)) by A1, Def33;

      let x be object;

      assume

       A3: x in ( dom (f1 <//> f4));

      then

       A4: x in ( dom f3) by A1, Def48;

      then

       A5: x in ( dom ( <-> f2)) by A1, XBOOLE_0:def 4;

      

      thus ((f1 <//> f4) . x) = ((f1 . x) /" (f4 . x)) by A3, Def48

      .= ((f1 . x) /" ( - (f2 . x))) by A5, Def33

      .= ( - ((f1 . x) /" (f2 . x))) by Th27

      .= ( - (f3 . x)) by A4, Def48

      .= (( <-> f3) . x) by A2, A3, Def33;

    end;

    theorem :: VALUED_2:93

    ((f <##> f1) <//> f2) = (f <##> (f1 <//> f2))

    proof

      set f3 = (f <##> f1), f4 = (f1 <//> f2);

      

       A1: ( dom (f3 <//> f2)) = (( dom f3) /\ ( dom f2)) by Def48;

      

       A2: ( dom (f <##> f4)) = (( dom f) /\ ( dom f4)) by Def47;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def47, Def48;

      hence

       A3: ( dom (f3 <//> f2)) = ( dom (f <##> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <//> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <//> f2) . x) = ((f3 . x) /" (f2 . x)) by A4, Def48

      .= (((f . x) (#) (f1 . x)) /" (f2 . x)) by A6, Def47

      .= ((f . x) (#) ((f1 . x) /" (f2 . x))) by Th19

      .= ((f . x) (#) (f4 . x)) by A5, Def48

      .= ((f <##> f4) . x) by A3, A4, Def47;

    end;

    theorem :: VALUED_2:94

    ((f <//> f1) <##> f2) = ((f <##> f2) <//> f1)

    proof

      set f3 = (f <//> f1), f4 = (f <##> f2);

      

       A1: ( dom (f3 <##> f2)) = (( dom f3) /\ ( dom f2)) by Def47;

      

       A2: ( dom (f4 <//> f1)) = (( dom f4) /\ ( dom f1)) by Def48;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f) /\ ( dom f2)) by Def47, Def48;

      hence

       A3: ( dom (f3 <##> f2)) = ( dom (f4 <//> f1)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <##> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <##> f2) . x) = ((f3 . x) (#) (f2 . x)) by A4, Def47

      .= (((f . x) /" (f1 . x)) (#) (f2 . x)) by A6, Def48

      .= (((f . x) (#) (f2 . x)) /" (f1 . x)) by Th20

      .= ((f4 . x) /" (f1 . x)) by A5, Def47

      .= ((f4 <//> f1) . x) by A3, A4, Def48;

    end;

    theorem :: VALUED_2:95

    ((f <//> f1) <//> f2) = (f <//> (f1 <##> f2))

    proof

      set f3 = (f <//> f1), f4 = (f1 <##> f2);

      

       A1: ( dom (f3 <//> f2)) = (( dom f3) /\ ( dom f2)) by Def48;

      

       A2: ( dom (f <//> f4)) = (( dom f) /\ ( dom f4)) by Def48;

      ( dom f3) = (( dom f) /\ ( dom f1)) & ( dom f4) = (( dom f1) /\ ( dom f2)) by Def47, Def48;

      hence

       A3: ( dom (f3 <//> f2)) = ( dom (f <//> f4)) by A1, A2, XBOOLE_1: 16;

      let x be object;

      assume

       A4: x in ( dom (f3 <//> f2));

      then

       A5: x in ( dom f4) by A2, A3, XBOOLE_0:def 4;

      

       A6: x in ( dom f3) by A1, A4, XBOOLE_0:def 4;

      

      thus ((f3 <//> f2) . x) = ((f3 . x) /" (f2 . x)) by A4, Def48

      .= (((f . x) /" (f1 . x)) /" (f2 . x)) by A6, Def48

      .= ((f . x) /" ((f1 . x) (#) (f2 . x))) by Th21

      .= ((f . x) /" (f4 . x)) by A5, Def47

      .= ((f <//> f4) . x) by A3, A4, Def48;

    end;

    theorem :: VALUED_2:96

    ((f1 <++> f2) <//> f) = ((f1 <//> f) <++> (f2 <//> f))

    proof

      set f3 = (f1 <//> f), f4 = (f2 <//> f), f5 = (f1 <++> f2);

      

       A1: ( dom (f5 <//> f)) = (( dom f) /\ ( dom f5)) by Def48;

      

       A2: ( dom f5) = (( dom f1) /\ ( dom f2)) by Def45;

      

       A3: ( dom (f3 <++> f4)) = (( dom f3) /\ ( dom f4)) by Def45;

      ( dom f3) = (( dom f1) /\ ( dom f)) & ( dom f4) = (( dom f2) /\ ( dom f)) by Def48;

      hence

       A4: ( dom (f5 <//> f)) = ( dom (f3 <++> f4)) by A1, A3, A2, Lm1;

      let x be object;

      assume

       A5: x in ( dom (f5 <//> f));

      then

       A6: x in ( dom f3) by A3, A4, XBOOLE_0:def 4;

      

       A7: x in ( dom f5) by A1, A5, XBOOLE_0:def 4;

      

       A8: x in ( dom f4) by A3, A4, A5, XBOOLE_0:def 4;

      

      thus ((f5 <//> f) . x) = ((f5 . x) /" (f . x)) by A5, Def48

      .= (((f1 . x) + (f2 . x)) /" (f . x)) by A7, Def45

      .= (((f1 . x) /" (f . x)) + ((f2 . x) /" (f . x))) by RFUNCT_1: 10

      .= ((f3 . x) + ((f2 . x) /" (f . x))) by A6, Def48

      .= ((f3 . x) + (f4 . x)) by A8, Def48

      .= ((f3 <++> f4) . x) by A4, A5, Def45;

    end;

    theorem :: VALUED_2:97

    ((f1 <--> f2) <//> f) = ((f1 <//> f) <--> (f2 <//> f))

    proof

      set f3 = (f1 <//> f), f4 = (f2 <//> f), f5 = (f1 <--> f2);

      

       A1: ( dom (f5 <//> f)) = (( dom f) /\ ( dom f5)) by Def48;

      

       A2: ( dom f5) = (( dom f1) /\ ( dom f2)) by Def46;

      

       A3: ( dom (f3 <--> f4)) = (( dom f3) /\ ( dom f4)) by Def46;

      ( dom f3) = (( dom f1) /\ ( dom f)) & ( dom f4) = (( dom f2) /\ ( dom f)) by Def48;

      hence

       A4: ( dom (f5 <//> f)) = ( dom (f3 <--> f4)) by A1, A3, A2, Lm1;

      let x be object;

      assume

       A5: x in ( dom (f5 <//> f));

      then

       A6: x in ( dom f3) by A3, A4, XBOOLE_0:def 4;

      

       A7: x in ( dom f5) by A1, A5, XBOOLE_0:def 4;

      

       A8: x in ( dom f4) by A3, A4, A5, XBOOLE_0:def 4;

      

      thus ((f5 <//> f) . x) = ((f5 . x) /" (f . x)) by A5, Def48

      .= (((f1 . x) - (f2 . x)) /" (f . x)) by A7, Def46

      .= (((f1 . x) /" (f . x)) - ((f2 . x) /" (f . x))) by RFUNCT_1: 14

      .= ((f3 . x) - ((f2 . x) /" (f . x))) by A6, Def48

      .= ((f3 . x) - (f4 . x)) by A8, Def48

      .= ((f3 <--> f4) . x) by A4, A5, Def46;

    end;