fuzzy_1.miz



    begin

    reserve x,y,y1,y2 for set;

    reserve C for non empty set;

    reserve c for Element of C;

    registration

      let x, y;

      cluster ( chi (x,y)) -> [. 0 , 1.] -valued;

      coherence

      proof

        1 in [. 0 , 1.] & 0 in [. 0 , 1.] by XXREAL_1: 1;

        then ( rng ( chi (x,y))) c= { 0 , 1} & { 0 , 1} c= [. 0 , 1.] by FUNCT_3: 39, ZFMISC_1: 32;

        hence ( rng ( chi (x,y))) c= [. 0 , 1.] by XBOOLE_1: 1;

      end;

    end

    registration

      let C;

      cluster [. 0 , 1.] -valued for Function of C, REAL ;

      existence

      proof

        take ( chi (C,C));

        thus ( rng ( chi (C,C))) c= [. 0 , 1.] by RELAT_1:def 19;

      end;

    end

    definition

      let C;

      mode Membership_Func of C is [. 0 , 1.] -valued Function of C, REAL ;

    end

    theorem :: FUZZY_1:1

    ( chi (C,C)) is Membership_Func of C;

    reserve f,h,g,h1 for Membership_Func of C;

    registration

      let X be non empty set;

      cluster -> real-valued for Membership_Func of X;

      coherence ;

    end

    definition

      let f,g be real-valued Function;

      :: FUZZY_1:def1

      pred f is_less_than g means ( dom f) c= ( dom g) & for x be set st x in ( dom f) holds (f . x) <= (g . x);

      reflexivity ;

    end

    notation

      let X be non empty set;

      let f,g be Membership_Func of X;

      synonym f c= g for f is_less_than g;

    end

    definition

      let X be non empty set;

      let f,g be Membership_Func of X;

      :: original: is_less_than

      redefine

      :: FUZZY_1:def2

      pred f is_less_than g means

      : Def2: for x be Element of X holds (f . x) <= (g . x);

      compatibility

      proof

        thus f is_less_than g iff for x be Element of X holds (f . x) <= (g . x)

        proof

          hereby

            assume

             A1: f is_less_than g;

            thus for x be Element of X holds (f . x) <= (g . x)

            proof

              let x be Element of X;

              ( dom f) = X by FUNCT_2:def 1;

              hence thesis by A1;

            end;

          end;

          assume for x be Element of X holds (f . x) <= (g . x);

          then ( dom g) = X & for x be set st x in ( dom f) holds (f . x) <= (g . x) by FUNCT_2:def 1;

          hence thesis;

        end;

      end;

    end

    

     Lm1: f c= g & g c= f implies f = g

    proof

      set A = f, B = g;

      assume

       A1: A c= B & B c= A;

      

       A2: for c be Element of C st c in C holds (f . c) = (g . c)

      proof

        let c be Element of C;

        (f . c) <= (g . c) & (g . c) <= (f . c) by A1;

        hence thesis by XXREAL_0: 1;

      end;

      C = ( dom f) & C = ( dom g) by FUNCT_2:def 1;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:2

    f = g iff f c= g & g c= f by Lm1;

    theorem :: FUZZY_1:3

    f c= f;

    theorem :: FUZZY_1:4

    f c= g & g c= h implies g c= h;

    begin

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    definition

      let C be non empty set;

      let h,g be Membership_Func of C;

      :: FUZZY_1:def3

      func min (h,g) -> Membership_Func of C means

      : Def3: for c be Element of C holds (it . c) = ( min ((h . c),(g . c)));

      existence

      proof

        defpred P[ object, object] means $2 = ( min ((h . $1),(g . $1)));

        

         A1: for x,y1,y2 be object st x in C & P[x, y1] & P[x, y2] holds y1 = y2;

        

         A2: for x,y be object st x in C & P[x, y] holds y in REAL by XREAL_0:def 1;

        consider IT be PartFunc of C, REAL such that

         A3: (for x be object holds x in ( dom IT) iff x in C & ex y be object st P[x, y]) & for x be object st x in ( dom IT) holds P[x, (IT . x)] from PARTFUN1:sch 2( A2, A1);

        for x be object st x in C holds x in ( dom IT)

        proof

          let x be object;

          ( min ((h . x),(g . x))) is set by TARSKI: 1;

          hence thesis by A3;

        end;

        then C c= ( dom IT) by TARSKI:def 3;

        then

         A5: ( dom IT) = C by XBOOLE_0:def 10;

        then

         A6: for c be Element of C holds (IT . c) = ( min ((h . c),(g . c))) by A3;

        

         A7: ( rng h) c= [. 0 , 1.] by RELAT_1:def 19;

        

         A8: ( rng g) c= [. 0 , 1.] by RELAT_1:def 19;

        for y be object st y in ( rng IT) holds y in [. 0 , 1.]

        proof

          reconsider A = [. 0 , jj.] as non empty closed_interval Subset of REAL by MEASURE5: 14;

          let y be object;

          assume y in ( rng IT);

          then

          consider x be Element of C such that

           A9: x in ( dom IT) and

           A10: y = (IT . x) by PARTFUN1: 3;

          

           A11: (h . x) >= ( min ((h . x),(g . x))) by XXREAL_0: 17;

          

           A12: A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

          then

           A13: 0 = ( lower_bound A) by INTEGRA1: 5;

          

           A14: x in C;

          then x in ( dom h) by FUNCT_2:def 1;

          then

           A15: (h . x) in ( rng h) by FUNCT_1:def 3;

          

           A16: 1 = ( upper_bound A) by A12, INTEGRA1: 5;

          then (h . x) <= 1 by A7, A15, INTEGRA2: 1;

          then ( min ((h . x),(g . x))) <= 1 by A11, XXREAL_0: 2;

          then

           A17: (IT . x) <= 1 by A3, A9;

          x in ( dom g) by A14, FUNCT_2:def 1;

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

          then

           A18: 0 <= (g . x) by A8, A13, INTEGRA2: 1;

           0 <= (h . x) by A7, A13, A15, INTEGRA2: 1;

          then 0 <= ( min ((h . x),(g . x))) by A18, XXREAL_0: 20;

          then 0 <= (IT . x) by A3, A9;

          hence thesis by A10, A13, A16, A17, INTEGRA2: 1;

        end;

        then

         A19: ( rng IT) c= [. 0 , 1.] by TARSKI:def 3;

        IT is total by A5, PARTFUN1:def 2;

        then IT is Membership_Func of C by A19, RELAT_1:def 19;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let F,G be Membership_Func of C;

        assume that

         A20: for c be Element of C holds (F . c) = ( min ((h . c),(g . c))) and

         A21: for c be Element of C holds (G . c) = ( min ((h . c),(g . c)));

        

         A22: for c be Element of C st c in C holds (F . c) = (G . c)

        proof

          let c be Element of C;

          (F . c) = ( min ((h . c),(g . c))) by A20;

          hence thesis by A21;

        end;

        C = ( dom F) & C = ( dom G) by FUNCT_2:def 1;

        hence thesis by A22, PARTFUN1: 5;

      end;

      idempotence ;

      commutativity ;

    end

    definition

      let C be non empty set;

      let h,g be Membership_Func of C;

      :: FUZZY_1:def4

      func max (h,g) -> Membership_Func of C means

      : Def4: for c be Element of C holds (it . c) = ( max ((h . c),(g . c)));

      existence

      proof

        defpred P[ object, object] means $2 = ( max ((h . $1),(g . $1)));

        

         A1: for x,y1,y2 be object st x in C & P[x, y1] & P[x, y2] holds y1 = y2;

        

         A2: for x,y be object st x in C & P[x, y] holds y in REAL by XREAL_0:def 1;

        consider IT be PartFunc of C, REAL such that

         A3: (for x be object holds x in ( dom IT) iff x in C & ex y be object st P[x, y]) & for x be object st x in ( dom IT) holds P[x, (IT . x)] from PARTFUN1:sch 2( A2, A1);

        for x be object st x in C holds x in ( dom IT)

        proof

          let x be object;

          ( max ((h . x),(g . x))) is set by TARSKI: 1;

          hence thesis by A3;

        end;

        then C c= ( dom IT) by TARSKI:def 3;

        then

         A5: ( dom IT) = C by XBOOLE_0:def 10;

        then

         A6: for c be Element of C holds (IT . c) = ( max ((h . c),(g . c))) by A3;

        

         A7: ( rng h) c= [. 0 , 1.] by RELAT_1:def 19;

        

         A8: ( rng g) c= [. 0 , 1.] by RELAT_1:def 19;

        for y be object st y in ( rng IT) holds y in [. 0 , 1.]

        proof

          reconsider A = [. 0 , jj.] as non empty closed_interval Subset of REAL by MEASURE5: 14;

          let y be object;

          assume y in ( rng IT);

          then

          consider x be Element of C such that

           A9: x in ( dom IT) and

           A10: y = (IT . x) by PARTFUN1: 3;

          

           A11: A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

          then

           A12: 0 = ( lower_bound A) by INTEGRA1: 5;

          

           A13: x in C;

          then x in ( dom h) by FUNCT_2:def 1;

          then

           A14: (h . x) in ( rng h) by FUNCT_1:def 3;

          then 0 <= (h . x) by A7, A12, INTEGRA2: 1;

          then 0 <= ( max ((h . x),(g . x))) by XXREAL_0: 30;

          then

           A15: 0 <= (IT . x) by A3, A9;

          

           A16: 1 = ( upper_bound A) by A11, INTEGRA1: 5;

          x in ( dom g) by A13, FUNCT_2:def 1;

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

          then

           A17: (g . x) <= 1 by A8, A16, INTEGRA2: 1;

          (h . x) <= 1 by A7, A16, A14, INTEGRA2: 1;

          then ( max ((h . x),(g . x))) <= 1 by A17, XXREAL_0: 28;

          then (IT . x) <= 1 by A3, A9;

          hence thesis by A10, A12, A16, A15, INTEGRA2: 1;

        end;

        then

         A18: ( rng IT) c= [. 0 , 1.] by TARSKI:def 3;

        IT is total by A5, PARTFUN1:def 2;

        then IT is Membership_Func of C by A18, RELAT_1:def 19;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let F,G be Membership_Func of C;

        assume that

         A19: for c be Element of C holds (F . c) = ( max ((h . c),(g . c))) and

         A20: for c be Element of C holds (G . c) = ( max ((h . c),(g . c)));

        

         A21: for c be Element of C st c in C holds (F . c) = (G . c)

        proof

          let c be Element of C;

          (F . c) = ( max ((h . c),(g . c))) by A19;

          hence thesis by A20;

        end;

        C = ( dom F) & C = ( dom G) by FUNCT_2:def 1;

        hence thesis by A21, PARTFUN1: 5;

      end;

      idempotence ;

      commutativity ;

    end

    definition

      let C be non empty set;

      let h be Membership_Func of C;

      :: FUZZY_1:def5

      func 1_minus h -> Membership_Func of C means

      : Def5: for c be Element of C holds (it . c) = (1 - (h . c));

      existence

      proof

        deffunc F( set) = ( In ((1 - (h . $1)), REAL ));

        defpred P[ set] means $1 in ( dom h);

        consider IT be PartFunc of C, REAL such that

         A1: (for x be Element of C holds x in ( dom IT) iff P[x]) & for x be Element of C st x in ( dom IT) holds (IT . x) = F(x) from SEQ_1:sch 3;

        for x be object st x in C holds x in ( dom IT)

        proof

          let x be object;

          

           A2: ( dom h) = C by FUNCT_2:def 1;

          assume x in C;

          hence thesis by A1, A2;

        end;

        then C c= ( dom IT) by TARSKI:def 3;

        then

         A3: ( dom IT) = C by XBOOLE_0:def 10;

        then

         A4: for c be Element of C holds (IT . c) = F(c) by A1;

        

         A5: ( rng h) c= [. 0 , 1.] by RELAT_1:def 19;

        for y be object st y in ( rng IT) holds y in [. 0 , 1.]

        proof

          reconsider A = [. 0 , jj.] as non empty closed_interval Subset of REAL by MEASURE5: 14;

          let y be object;

          assume y in ( rng IT);

          then

          consider x be Element of C such that

           A6: x in ( dom IT) and

           A7: y = (IT . x) by PARTFUN1: 3;

          

           A8: A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

          then

           A9: 0 = ( lower_bound A) by INTEGRA1: 5;

          x in C;

          then x in ( dom h) by FUNCT_2:def 1;

          then

           A10: (h . x) in ( rng h) by FUNCT_1:def 3;

          then 0 <= (h . x) by A5, A9, INTEGRA2: 1;

          then ( 0 + 1) <= (1 + (h . x)) by XREAL_1: 6;

          then F(x) <= 1 by XREAL_1: 20;

          then

           A11: (IT . x) <= 1 by A1, A6;

          

           A12: 1 = ( upper_bound A) by A8, INTEGRA1: 5;

          then (h . x) <= 1 by A5, A10, INTEGRA2: 1;

          then 0 <= F(x) by XREAL_1: 48;

          then 0 <= (IT . x) by A1, A6;

          hence thesis by A7, A9, A12, A11, INTEGRA2: 1;

        end;

        then

         A13: ( rng IT) c= [. 0 , 1.] by TARSKI:def 3;

        IT is total by A3, PARTFUN1:def 2;

        then

        reconsider IT as Membership_Func of C by A13, RELAT_1:def 19;

        take IT;

        let c be Element of C;

        (IT . c) = F(c) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Membership_Func of C;

        assume that

         A14: for c be Element of C holds (F . c) = (1 - (h . c)) and

         A15: for c be Element of C holds (G . c) = (1 - (h . c));

        

         A16: for c be Element of C st c in C holds (F . c) = (G . c)

        proof

          let c be Element of C;

          (F . c) = (1 - (h . c)) by A14;

          hence thesis by A15;

        end;

        C = ( dom F) & C = ( dom G) by FUNCT_2:def 1;

        hence thesis by A16, PARTFUN1: 5;

      end;

      involutiveness

      proof

        let h1,h2 be Membership_Func of C;

        assume

         A17: for c be Element of C holds (h1 . c) = (1 - (h2 . c));

        let c be Element of C;

        

        thus (h2 . c) = (1 - (1 - (h2 . c)))

        .= (1 - (h1 . c)) by A17;

      end;

    end

    theorem :: FUZZY_1:5

    ( min ((h . c),(g . c))) = (( min (h,g)) . c) & ( max ((h . c),(g . c))) = (( max (h,g)) . c) by Def3, Def4;

    theorem :: FUZZY_1:6

    ( max (h,h)) = h & ( min (h,h)) = h & ( max (h,h)) = ( min (h,h)) & ( min (f,g)) = ( min (g,f)) & ( max (f,g)) = ( max (g,f));

    theorem :: FUZZY_1:7

    

     Th7: ( max (( max (f,g)),h)) = ( max (f,( max (g,h)))) & ( min (( min (f,g)),h)) = ( min (f,( min (g,h))))

    proof

      

       A1: C = ( dom ( min (( min (f,g)),h))) & C = ( dom ( min (f,( min (g,h))))) by FUNCT_2:def 1;

      

       A2: for x be Element of C st x in C holds (( max (( max (f,g)),h)) . x) = (( max (f,( max (g,h)))) . x)

      proof

        let x be Element of C;

        (( max (( max (f,g)),h)) . x) = ( max ((( max (f,g)) . x),(h . x))) by Def4

        .= ( max (( max ((f . x),(g . x))),(h . x))) by Def4

        .= ( max ((f . x),( max ((g . x),(h . x))))) by XXREAL_0: 34

        .= ( max ((f . x),(( max (g,h)) . x))) by Def4

        .= (( max (f,( max (g,h)))) . x) by Def4;

        hence thesis;

      end;

      

       A3: for x be Element of C st x in C holds (( min (( min (f,g)),h)) . x) = (( min (f,( min (g,h)))) . x)

      proof

        let x be Element of C;

        (( min (( min (f,g)),h)) . x) = ( min ((( min (f,g)) . x),(h . x))) by Def3

        .= ( min (( min ((f . x),(g . x))),(h . x))) by Def3

        .= ( min ((f . x),( min ((g . x),(h . x))))) by XXREAL_0: 33

        .= ( min ((f . x),(( min (g,h)) . x))) by Def3

        .= (( min (f,( min (g,h)))) . x) by Def3;

        hence thesis;

      end;

      C = ( dom ( max (( max (f,g)),h))) & C = ( dom ( max (f,( max (g,h))))) by FUNCT_2:def 1;

      hence thesis by A1, A2, A3, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:8

    

     Th8: ( max (f,( min (f,g)))) = f & ( min (f,( max (f,g)))) = f

    proof

      

       A1: C = ( dom ( min (f,( max (f,g))))) by FUNCT_2:def 1;

      

       A2: for x be Element of C st x in C holds (( max (f,( min (f,g)))) . x) = (f . x)

      proof

        let x be Element of C;

        (( max (f,( min (f,g)))) . x) = ( max ((f . x),(( min (f,g)) . x))) by Def4

        .= ( max ((f . x),( min ((f . x),(g . x))))) by Def3

        .= (f . x) by XXREAL_0: 36;

        hence thesis;

      end;

      

       A3: for x be Element of C st x in C holds (( min (f,( max (f,g)))) . x) = (f . x)

      proof

        let x be Element of C;

        (( min (f,( max (f,g)))) . x) = ( min ((f . x),(( max (f,g)) . x))) by Def3

        .= ( min ((f . x),( max ((f . x),(g . x))))) by Def4

        .= (f . x) by XXREAL_0: 35;

        hence thesis;

      end;

      C = ( dom ( max (f,( min (f,g))))) & C = ( dom f) by FUNCT_2:def 1;

      hence thesis by A1, A2, A3, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:9

    

     Th9: ( min (f,( max (g,h)))) = ( max (( min (f,g)),( min (f,h)))) & ( max (f,( min (g,h)))) = ( min (( max (f,g)),( max (f,h))))

    proof

      

       A1: C = ( dom ( max (f,( min (g,h))))) & C = ( dom ( min (( max (f,g)),( max (f,h))))) by FUNCT_2:def 1;

      

       A2: for x be Element of C st x in C holds (( min (f,( max (g,h)))) . x) = (( max (( min (f,g)),( min (f,h)))) . x)

      proof

        let x be Element of C;

        (( min (f,( max (g,h)))) . x) = ( min ((f . x),(( max (g,h)) . x))) by Def3

        .= ( min ((f . x),( max ((g . x),(h . x))))) by Def4

        .= ( max (( min ((f . x),(g . x))),( min ((f . x),(h . x))))) by XXREAL_0: 38

        .= ( max ((( min (f,g)) . x),( min ((f . x),(h . x))))) by Def3

        .= ( max ((( min (f,g)) . x),(( min (f,h)) . x))) by Def3

        .= (( max (( min (f,g)),( min (f,h)))) . x) by Def4;

        hence thesis;

      end;

      

       A3: for x be Element of C st x in C holds (( max (f,( min (g,h)))) . x) = (( min (( max (f,g)),( max (f,h)))) . x)

      proof

        let x be Element of C;

        (( max (f,( min (g,h)))) . x) = ( max ((f . x),(( min (g,h)) . x))) by Def4

        .= ( max ((f . x),( min ((g . x),(h . x))))) by Def3

        .= ( min (( max ((f . x),(g . x))),( max ((f . x),(h . x))))) by XXREAL_0: 39

        .= ( min ((( max (f,g)) . x),( max ((f . x),(h . x))))) by Def4

        .= ( min ((( max (f,g)) . x),(( max (f,h)) . x))) by Def4

        .= (( min (( max (f,g)),( max (f,h)))) . x) by Def3;

        hence thesis;

      end;

      C = ( dom ( min (f,( max (g,h))))) & C = ( dom ( max (( min (f,g)),( min (f,h))))) by FUNCT_2:def 1;

      hence thesis by A1, A2, A3, PARTFUN1: 5;

    end;

    ::$Canceled

    theorem :: FUZZY_1:11

    

     Th10: ( 1_minus ( max (f,g))) = ( min (( 1_minus f),( 1_minus g))) & ( 1_minus ( min (f,g))) = ( max (( 1_minus f),( 1_minus g)))

    proof

      

       A1: C = ( dom ( 1_minus ( min (f,g)))) & C = ( dom ( max (( 1_minus f),( 1_minus g)))) by FUNCT_2:def 1;

      

       A2: for x be Element of C st x in C holds (( 1_minus ( max (f,g))) . x) = (( min (( 1_minus f),( 1_minus g))) . x)

      proof

        let x be Element of C;

        

         A3: (( 1_minus ( max (f,g))) . x) = (1 - (( max (f,g)) . x)) by Def5

        .= (1 - ( max ((f . x),(g . x)))) by Def4

        .= (1 - ((((f . x) + (g . x)) + |.((f . x) - (g . x)).|) / 2)) by COMPLEX1: 74;

        (( min (( 1_minus f),( 1_minus g))) . x) = ( min ((( 1_minus f) . x),(( 1_minus g) . x))) by Def3

        .= ( min ((1 - (f . x)),(( 1_minus g) . x))) by Def5

        .= ( min ((1 - (f . x)),(1 - (g . x)))) by Def5

        .= ((((1 - (f . x)) + (1 - (g . x))) - |.((1 - (f . x)) - (1 - (g . x))).|) / 2) by COMPLEX1: 73

        .= ((((2 - (f . x)) - (g . x)) - |.( - ((f . x) - (g . x))).|) / 2)

        .= (((2 - ((f . x) + (g . x))) - |.((f . x) - (g . x)).|) / 2) by COMPLEX1: 52

        .= (1 - ((((f . x) + (g . x)) + |.((f . x) - (g . x)).|) / 2));

        hence thesis by A3;

      end;

      

       A4: for x be Element of C st x in C holds (( 1_minus ( min (f,g))) . x) = (( max (( 1_minus f),( 1_minus g))) . x)

      proof

        let x be Element of C;

        

         A5: (( 1_minus ( min (f,g))) . x) = (1 - (( min (f,g)) . x)) by Def5

        .= (1 - ( min ((f . x),(g . x)))) by Def3

        .= (1 - ((((f . x) + (g . x)) - |.((f . x) - (g . x)).|) / 2)) by COMPLEX1: 73;

        (( max (( 1_minus f),( 1_minus g))) . x) = ( max ((( 1_minus f) . x),(( 1_minus g) . x))) by Def4

        .= ( max ((1 - (f . x)),(( 1_minus g) . x))) by Def5

        .= ( max ((1 - (f . x)),(1 - (g . x)))) by Def5

        .= ((((1 - (f . x)) + (1 - (g . x))) + |.((1 - (f . x)) - (1 - (g . x))).|) / 2) by COMPLEX1: 74

        .= ((((2 - (f . x)) - (g . x)) + |.( - ((f . x) - (g . x))).|) / 2)

        .= (((2 - ((f . x) + (g . x))) + |.((f . x) - (g . x)).|) / 2) by COMPLEX1: 52

        .= (1 - ((((f . x) + (g . x)) - |.((f . x) - (g . x)).|) / 2));

        hence thesis by A5;

      end;

      C = ( dom ( 1_minus ( max (f,g)))) & C = ( dom ( min (( 1_minus f),( 1_minus g)))) by FUNCT_2:def 1;

      hence thesis by A1, A2, A4, PARTFUN1: 5;

    end;

    begin

    theorem :: FUZZY_1:12

    ( chi ( {} ,C)) is Membership_Func of C;

    definition

      let C be non empty set;

      :: FUZZY_1:def6

      func EMF (C) -> Membership_Func of C equals ( chi ( {} ,C));

      correctness ;

    end

    definition

      let C be non empty set;

      :: FUZZY_1:def7

      func UMF (C) -> Membership_Func of C equals ( chi (C,C));

      correctness ;

    end

    theorem :: FUZZY_1:13

    

     Th12: for a,b be Element of REAL , f be PartFunc of C, REAL st ( rng f) c= [.a, b.] & a <= b holds for x be Element of C st x in ( dom f) holds a <= (f . x) & (f . x) <= b

    proof

      let a,b be Element of REAL ;

      let f be PartFunc of C, REAL ;

      assume that

       A1: ( rng f) c= [.a, b.] and

       A2: a <= b;

      for x be Element of C st x in ( dom f) holds a <= (f . x) & (f . x) <= b

      proof

        reconsider A = [.a, b.] as non empty closed_interval Subset of REAL by A2, MEASURE5: 14;

        let x be Element of C;

        A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

        then

         A3: a = ( lower_bound A) & b = ( upper_bound A) by INTEGRA1: 5;

        assume x in ( dom f);

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

        hence thesis by A1, A3, INTEGRA2: 1;

      end;

      hence thesis;

    end;

    theorem :: FUZZY_1:14

    

     Th13: ( EMF C) c= f

    proof

      let x be Element of C;

      

       A1: ( rng f) c= [. 0 , jj.] by RELAT_1:def 19;

      ( dom f) = C & (( EMF C) . x) = 0 by FUNCT_2:def 1, FUNCT_3:def 3;

      hence thesis by A1, Th12;

    end;

    theorem :: FUZZY_1:15

    

     Th14: f c= ( UMF C)

    proof

      let x be Element of C;

      

       A1: 0 in REAL by XREAL_0:def 1;

      

       A2: ( rng f) c= [. 0 , 1.] by RELAT_1:def 19;

      ( dom f) = C & (( UMF C) . x) = 1 by FUNCT_2:def 1, FUNCT_3:def 3;

      hence thesis by A2, Th12, A1;

    end;

    theorem :: FUZZY_1:16

    

     Th15: for x be Element of C, h be Membership_Func of C holds (( EMF C) . x) <= (h . x) & (h . x) <= (( UMF C) . x) by Th13, Th14, Def2;

    theorem :: FUZZY_1:17

    

     Th16: ( min (f,g)) c= f & f c= ( max (f,g))

    proof

      thus ( min (f,g)) c= f

      proof

        let x be Element of C;

        (( min (f,g)) . x) = ( min ((f . x),(g . x))) by Def3;

        hence thesis by XXREAL_0: 17;

      end;

      let x be Element of C;

      (( max (f,g)) . x) = ( max ((f . x),(g . x))) by Def4;

      hence thesis by XXREAL_0: 25;

    end;

    theorem :: FUZZY_1:18

    

     Th17: ( max (f,( UMF C))) = ( UMF C) & ( min (f,( UMF C))) = f & ( max (f,( EMF C))) = f & ( min (f,( EMF C))) = ( EMF C)

    proof

      

       A1: C = ( dom ( max (f,( EMF C)))) & C = ( dom ( min (f,( EMF C)))) by FUNCT_2:def 1;

      

       A2: for x be Element of C st x in C holds (( min (f,( UMF C))) . x) = (f . x)

      proof

        let x be Element of C;

        

         A3: (f . x) <= (( UMF C) . x) by Th15;

        (( min (f,( UMF C))) . x) = ( min ((f . x),(( UMF C) . x))) by Def3

        .= (f . x) by A3, XXREAL_0:def 9;

        hence thesis;

      end;

      

       A4: for x be Element of C st x in C holds (( min (f,( EMF C))) . x) = (( EMF C) . x)

      proof

        let x be Element of C;

        

         A5: (( EMF C) . x) <= (f . x) by Th15;

        (( min (f,( EMF C))) . x) = ( min ((f . x),(( EMF C) . x))) by Def3

        .= (( EMF C) . x) by A5, XXREAL_0:def 9;

        hence thesis;

      end;

      

       A6: for x be Element of C st x in C holds (( max (f,( EMF C))) . x) = (f . x)

      proof

        let x be Element of C;

        

         A7: (( EMF C) . x) <= (f . x) by Th15;

        (( max (f,( EMF C))) . x) = ( max ((f . x),(( EMF C) . x))) by Def4

        .= (f . x) by A7, XXREAL_0:def 10;

        hence thesis;

      end;

      ( max (f,( UMF C))) c= ( UMF C) & ( UMF C) c= ( max (f,( UMF C))) by Th14, Th16;

      hence ( max (f,( UMF C))) = ( UMF C) by Lm1;

      

       A8: C = ( dom ( EMF C)) by FUNCT_2:def 1;

      C = ( dom ( min (f,( UMF C)))) & C = ( dom f) by FUNCT_2:def 1;

      hence thesis by A2, A6, A1, A8, A4, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:19

    

     Th18: f c= h & g c= h implies ( max (f,g)) c= h

    proof

      assume

       A1: f c= h & g c= h;

      let x be Element of C;

      

       A2: ( max ((f . x),(g . x))) = (( max (f,g)) . x) by Def4;

      (f . x) <= (h . x) & (g . x) <= (h . x) by A1;

      hence thesis by A2, XXREAL_0: 28;

    end;

    theorem :: FUZZY_1:20

    f c= g implies ( max (f,h)) c= ( max (g,h))

    proof

      assume

       A1: f c= g;

      let x be Element of C;

      (f . x) <= (g . x) by A1;

      then ( max ((f . x),(h . x))) <= ( max ((g . x),(h . x))) by XXREAL_0: 26;

      then ( max ((f . x),(h . x))) <= (( max (g,h)) . x) by Def4;

      hence thesis by Def4;

    end;

    theorem :: FUZZY_1:21

    f c= g & h c= h1 implies ( max (f,h)) c= ( max (g,h1))

    proof

      assume

       A1: f c= g & h c= h1;

      let x be Element of C;

      (f . x) <= (g . x) & (h . x) <= (h1 . x) by A1;

      then ( max ((f . x),(h . x))) <= ( max ((g . x),(h1 . x))) by XXREAL_0: 26;

      then (( max (f,h)) . x) <= ( max ((g . x),(h1 . x))) by Def4;

      hence thesis by Def4;

    end;

    theorem :: FUZZY_1:22

    f c= g implies ( max (f,g)) = g

    proof

      assume f c= g;

      then

       A1: ( max (f,g)) c= g by Th18;

      g c= ( max (f,g)) by Th16;

      hence thesis by A1, Lm1;

    end;

    theorem :: FUZZY_1:23

    ( min (f,g)) c= ( max (f,g))

    proof

      let x be Element of C;

      ( min ((f . x),(g . x))) <= (f . x) & (f . x) <= ( max ((f . x),(g . x))) by XXREAL_0: 17, XXREAL_0: 25;

      then ( min ((f . x),(g . x))) <= ( max ((f . x),(g . x))) by XXREAL_0: 2;

      then ( min ((f . x),(g . x))) <= (( max (f,g)) . x) by Def4;

      hence thesis by Def3;

    end;

    theorem :: FUZZY_1:24

    

     Th23: h c= f & h c= g implies h c= ( min (f,g))

    proof

      assume

       A1: h c= f & h c= g;

      let x be Element of C;

      (h . x) <= (f . x) & (h . x) <= (g . x) by A1;

      then (h . x) <= ( min ((f . x),(g . x))) by XXREAL_0: 20;

      hence thesis by Def3;

    end;

    theorem :: FUZZY_1:25

    f c= g implies ( min (f,h)) c= ( min (g,h))

    proof

      assume

       A1: f c= g;

      let x be Element of C;

      (f . x) <= (g . x) by A1;

      then ( min ((f . x),(h . x))) <= ( min ((g . x),(h . x))) by XXREAL_0: 18;

      then (( min (f,h)) . x) <= ( min ((g . x),(h . x))) by Def3;

      hence thesis by Def3;

    end;

    theorem :: FUZZY_1:26

    f c= g & h c= h1 implies ( min (f,h)) c= ( min (g,h1))

    proof

      assume

       A1: f c= g & h c= h1;

      let x be Element of C;

      (f . x) <= (g . x) & (h . x) <= (h1 . x) by A1;

      then ( min ((f . x),(h . x))) <= ( min ((g . x),(h1 . x))) by XXREAL_0: 18;

      then (( min (f,h)) . x) <= ( min ((g . x),(h1 . x))) by Def3;

      hence thesis by Def3;

    end;

    theorem :: FUZZY_1:27

    

     Th26: f c= g implies ( min (f,g)) = f

    proof

      assume

       A1: f c= g;

      

       A2: for x be Element of C st x in C holds (( min (f,g)) . x) = (f . x)

      proof

        let x be Element of C;

        (f . x) <= (g . x) by A1;

        

        then (f . x) = ( min ((f . x),(g . x))) by XXREAL_0:def 9

        .= (( min (f,g)) . x) by Def3;

        hence thesis;

      end;

      C = ( dom ( min (f,g))) & C = ( dom f) by FUNCT_2:def 1;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:28

    f c= g & f c= h & ( min (g,h)) = ( EMF C) implies f = ( EMF C)

    proof

      assume that

       A1: f c= g & f c= h and

       A2: ( min (g,h)) = ( EMF C);

      

       A3: for x be Element of C st x in C holds (f . x) = (( EMF C) . x)

      proof

        let x be Element of C;

        (f . x) <= (g . x) & (f . x) <= (h . x) by A1;

        then (f . x) <= ( min ((g . x),(h . x))) by XXREAL_0: 20;

        then

         A4: (f . x) <= (( min (g,h)) . x) by Def3;

        (( EMF C) . x) <= (f . x) by Th15;

        hence thesis by A2, A4, XXREAL_0: 1;

      end;

      C = ( dom f) & C = ( dom ( EMF C)) by FUNCT_2:def 1;

      hence thesis by A3, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:29

    ( max (( min (f,g)),( min (f,h)))) = f implies f c= ( max (g,h))

    proof

      assume

       A1: ( max (( min (f,g)),( min (f,h)))) = f;

      let x be Element of C;

      (( max (( min (f,g)),( min (f,h)))) . x) = ( max ((( min (f,g)) . x),(( min (f,h)) . x))) by Def4

      .= ( max ((( min (f,g)) . x),( min ((f . x),(h . x))))) by Def3

      .= ( max (( min ((f . x),(g . x))),( min ((f . x),(h . x))))) by Def3

      .= ( min ((f . x),( max ((g . x),(h . x))))) by XXREAL_0: 38;

      then (f . x) <= ( max ((g . x),(h . x))) by A1, XXREAL_0:def 9;

      hence thesis by Def4;

    end;

    theorem :: FUZZY_1:30

    f c= g & ( min (g,h)) = ( EMF C) implies ( min (f,h)) = ( EMF C)

    proof

      assume that

       A1: f c= g and

       A2: ( min (g,h)) = ( EMF C);

      

       A3: for x be Element of C st x in C holds (( min (f,h)) . x) = (( EMF C) . x)

      proof

        let x be Element of C;

        (f . x) <= (g . x) by A1;

        then ( min ((f . x),(h . x))) <= ( min ((g . x),(h . x))) by XXREAL_0: 18;

        then ( min ((f . x),(h . x))) <= (( min (g,h)) . x) by Def3;

        then

         A4: (( min (f,h)) . x) <= (( min (g,h)) . x) by Def3;

        (( EMF C) . x) <= (( min (f,h)) . x) by Th15;

        hence thesis by A2, A4, XXREAL_0: 1;

      end;

      C = ( dom ( min (f,h))) & C = ( dom ( EMF C)) by FUNCT_2:def 1;

      hence thesis by A3, PARTFUN1: 5;

    end;

    theorem :: FUZZY_1:31

    f c= ( EMF C) implies f = ( EMF C)

    proof

      ( EMF C) c= f by Th13;

      hence thesis by Lm1;

    end;

    theorem :: FUZZY_1:32

    ( max (f,g)) = ( EMF C) iff f = ( EMF C) & g = ( EMF C)

    proof

      thus ( max (f,g)) = ( EMF C) implies f = ( EMF C) & g = ( EMF C)

      proof

        assume

         A1: ( max (f,g)) = ( EMF C);

        

         A2: for x be Element of C st x in C holds (f . x) = (( EMF C) . x)

        proof

          let x be Element of C;

          ( max ((f . x),(g . x))) = (( EMF C) . x) by A1, Def4;

          then

           A3: (f . x) <= (( EMF C) . x) by XXREAL_0: 25;

          (( EMF C) . x) <= (f . x) by Th15;

          hence thesis by A3, XXREAL_0: 1;

        end;

        

         A4: for x be Element of C st x in C holds (g . x) = (( EMF C) . x)

        proof

          let x be Element of C;

          ( max ((f . x),(g . x))) = (( EMF C) . x) by A1, Def4;

          then

           A5: (g . x) <= (( EMF C) . x) by XXREAL_0: 25;

          (( EMF C) . x) <= (g . x) by Th15;

          hence thesis by A5, XXREAL_0: 1;

        end;

        C = ( dom f) & C = ( dom ( EMF C)) by FUNCT_2:def 1;

        hence f = ( EMF C) by A2, PARTFUN1: 5;

        C = ( dom g) & C = ( dom ( EMF C)) by FUNCT_2:def 1;

        hence g = ( EMF C) by A4, PARTFUN1: 5;

      end;

      assume f = ( EMF C) & g = ( EMF C);

      hence thesis;

    end;

    theorem :: FUZZY_1:33

    f = ( max (g,h)) iff g c= f & h c= f & for h1 st g c= h1 & h c= h1 holds f c= h1

    proof

      hereby

        assume

         A1: f = ( max (g,h));

        hence g c= f & h c= f by Th16;

        let h1;

        assume

         A2: g c= h1 & h c= h1;

        thus f c= h1

        proof

          let x be Element of C;

          (g . x) <= (h1 . x) & (h . x) <= (h1 . x) by A2;

          then ( max ((g . x),(h . x))) <= (h1 . x) by XXREAL_0: 28;

          hence thesis by A1, Def4;

        end;

      end;

      assume that

       A3: g c= f & h c= f and

       A4: for h1 st g c= h1 & h c= h1 holds f c= h1;

      g c= ( max (g,h)) & h c= ( max (g,h)) by Th16;

      then

       A5: f c= ( max (g,h)) by A4;

      ( max (g,h)) c= f by A3, Th18;

      hence thesis by A5, Lm1;

    end;

    theorem :: FUZZY_1:34

    f = ( min (g,h)) iff f c= g & f c= h & for h1 st h1 c= g & h1 c= h holds h1 c= f

    proof

      hereby

        assume

         A1: f = ( min (g,h));

        hence f c= g & f c= h by Th16;

        let h1;

        assume

         A2: h1 c= g & h1 c= h;

        thus h1 c= f

        proof

          let x be Element of C;

          (h1 . x) <= (g . x) & (h1 . x) <= (h . x) by A2;

          then ( min ((g . x),(h . x))) >= (h1 . x) by XXREAL_0: 20;

          hence thesis by A1, Def3;

        end;

      end;

      assume that

       A3: f c= g & f c= h and

       A4: for h1 st h1 c= g & h1 c= h holds h1 c= f;

      ( min (g,h)) c= g & ( min (g,h)) c= h by Th16;

      then

       A5: ( min (g,h)) c= f by A4;

      f c= ( min (g,h)) by A3, Th23;

      hence thesis by A5, Lm1;

    end;

    theorem :: FUZZY_1:35

    f c= ( max (g,h)) & ( min (f,h)) = ( EMF C) implies f c= g

    proof

      assume that

       A1: f c= ( max (g,h)) and

       A2: ( min (f,h)) = ( EMF C);

      let x be Element of C;

      ( min (f,( max (g,h)))) = f by A1, Th26;

      

      then f = ( max (( min (f,g)),( min (f,h)))) by Th9

      .= ( min (f,g)) by A2, Th17;

      then (f . x) = ( min ((f . x),(g . x))) by Def3;

      hence thesis by XXREAL_0:def 9;

    end;

    

     Lm2: f c= g implies ( 1_minus g) c= ( 1_minus f)

    proof

      assume

       A1: f c= g;

      let x be Element of C;

      (f . x) <= (g . x) by A1;

      then (1 - (g . x)) <= (1 - (f . x)) by XREAL_1: 10;

      then (( 1_minus g) . x) <= (1 - (f . x)) by Def5;

      hence thesis by Def5;

    end;

    theorem :: FUZZY_1:36

    

     Th35: f c= g iff ( 1_minus g) c= ( 1_minus f)

    proof

      ( 1_minus ( 1_minus f)) = f & ( 1_minus ( 1_minus g)) = g;

      hence thesis by Lm2;

    end;

    theorem :: FUZZY_1:37

    f c= ( 1_minus g) implies g c= ( 1_minus f)

    proof

      ( 1_minus ( 1_minus f)) = f;

      hence thesis by Th35;

    end;

    theorem :: FUZZY_1:38

    ( 1_minus ( max (f,g))) c= ( 1_minus f) by Th16, Th35;

    theorem :: FUZZY_1:39

    ( 1_minus f) c= ( 1_minus ( min (f,g))) by Th16, Th35;

    theorem :: FUZZY_1:40

    

     Th39: ( 1_minus ( EMF C)) = ( UMF C) & ( 1_minus ( UMF C)) = ( EMF C)

    proof

      

       A1: for x be Element of C st x in C holds (( 1_minus ( EMF C)) . x) = (( UMF C) . x)

      proof

        let x be Element of C;

        (( 1_minus ( EMF C)) . x) = (1 - (( EMF C) . x)) by Def5

        .= (1 - 0 ) by FUNCT_3:def 3

        .= 1;

        hence thesis by FUNCT_3:def 3;

      end;

      C = ( dom ( 1_minus ( EMF C))) & C = ( dom ( UMF C)) by FUNCT_2:def 1;

      hence ( 1_minus ( EMF C)) = ( UMF C) by A1, PARTFUN1: 5;

      

       A2: for x be Element of C st x in C holds (( 1_minus ( UMF C)) . x) = (( EMF C) . x)

      proof

        let x be Element of C;

        (( 1_minus ( UMF C)) . x) = (1 - (( UMF C) . x)) by Def5

        .= (1 - 1) by FUNCT_3:def 3

        .= 0 ;

        hence thesis by FUNCT_3:def 3;

      end;

      C = ( dom ( 1_minus ( UMF C))) & C = ( dom ( EMF C)) by FUNCT_2:def 1;

      hence thesis by A2, PARTFUN1: 5;

    end;

    definition

      let C be non empty set;

      let h,g be Membership_Func of C;

      :: FUZZY_1:def8

      func h \+\ g -> Membership_Func of C equals ( max (( min (h,( 1_minus g))),( min (( 1_minus h),g))));

      coherence ;

      commutativity ;

    end

    theorem :: FUZZY_1:41

    (f \+\ ( EMF C)) = f

    proof

      

      thus (f \+\ ( EMF C)) = ( max (( min (f,( UMF C))),( min (( 1_minus f),( EMF C))))) by Th39

      .= ( max (f,( min (( 1_minus f),( EMF C))))) by Th17

      .= ( max (f,( EMF C))) by Th17

      .= f by Th17;

    end;

    theorem :: FUZZY_1:42

    (f \+\ ( UMF C)) = ( 1_minus f)

    proof

      

      thus (f \+\ ( UMF C)) = ( max (( min (f,( EMF C))),( min (( 1_minus f),( UMF C))))) by Th39

      .= ( max (( EMF C),( min (( 1_minus f),( UMF C))))) by Th17

      .= ( min (( 1_minus f),( UMF C))) by Th17

      .= ( 1_minus f) by Th17;

    end;

    theorem :: FUZZY_1:43

    ( min (( min (( max (f,g)),( max (g,h)))),( max (h,f)))) = ( max (( max (( min (f,g)),( min (g,h)))),( min (h,f))))

    proof

      

      thus ( min (( min (( max (f,g)),( max (g,h)))),( max (h,f)))) = ( max (( min (( min (( max (f,g)),( max (g,h)))),h)),( min (( min (( max (f,g)),( max (g,h)))),f)))) by Th9

      .= ( max (( min (( max (f,g)),( min (( max (g,h)),h)))),( min (( min (( max (f,g)),( max (g,h)))),f)))) by Th7

      .= ( max (( min (( max (f,g)),( min (( max (h,g)),h)))),( min (( min (( max (f,g)),f)),( max (g,h)))))) by Th7

      .= ( max (( min (( max (f,g)),h)),( min (( min (( max (f,g)),f)),( max (g,h)))))) by Th8

      .= ( max (( min (( max (f,g)),h)),( min (f,( max (g,h)))))) by Th8

      .= ( max (( min (h,( max (f,g)))),( max (( min (f,g)),( min (f,h)))))) by Th9

      .= ( max (( max (( min (f,g)),( min (f,h)))),( max (( min (h,f)),( min (h,g)))))) by Th9

      .= ( max (( max (( max (( min (f,g)),( min (f,h)))),( min (f,h)))),( min (h,g)))) by Th7

      .= ( max (( max (( min (f,g)),( max (( min (f,h)),( min (f,h)))))),( min (h,g)))) by Th7

      .= ( max (( max (( min (f,g)),( min (g,h)))),( min (h,f)))) by Th7;

    end;

    theorem :: FUZZY_1:44

    ( max (( min (f,g)),( min (( 1_minus f),( 1_minus g))))) c= ( 1_minus (f \+\ g))

    proof

      set f1 = ( 1_minus f), g1 = ( 1_minus g);

      let x be Element of C;

      ( 1_minus (f \+\ g)) = ( min (( 1_minus ( min (f,g1))),( 1_minus ( min (f1,g))))) by Th10

      .= ( min (( max (f1,( 1_minus g1))),( 1_minus ( min (f1,g))))) by Th10

      .= ( min (( max (f1,g)),( max (( 1_minus f1),g1)))) by Th10

      .= ( max (( min (( max (f1,g)),f)),( min (( max (f1,g)),g1)))) by Th9

      .= ( max (( max (( min (f,f1)),( min (f,g)))),( min (( max (f1,g)),g1)))) by Th9

      .= ( max (( max (( min (f,f1)),( min (f,g)))),( max (( min (g1,f1)),( min (g1,g)))))) by Th9

      .= ( max (( max (( max (( min (f,g)),( min (f,f1)))),( min (g1,f1)))),( min (g1,g)))) by Th7

      .= ( max (( max (( max (( min (g1,f1)),( min (f,g)))),( min (f,f1)))),( min (g1,g)))) by Th7

      .= ( max (( max (( min (g1,f1)),( min (f,g)))),( max (( min (f,f1)),( min (g1,g)))))) by Th7;

      then (( 1_minus (f \+\ g)) . x) = ( max ((( max (( min (f,g)),( min (f1,g1)))) . x),(( max (( min (f,f1)),( min (g1,g)))) . x))) by Def4;

      hence thesis by XXREAL_0: 25;

    end;

    theorem :: FUZZY_1:45

    ( max ((f \+\ g),( min (f,g)))) c= ( max (f,g))

    proof

      set f1 = ( 1_minus f), g1 = ( 1_minus g);

      let x be Element of C;

      ( max ((f \+\ g),( min (f,g)))) = ( max (( min (f,g1)),( max (( min (f1,g)),( min (f,g)))))) by Th7

      .= ( max (( min (f,g1)),( min (( max (( min (f1,g)),f)),( max (g,( min (f1,g)))))))) by Th9

      .= ( max (( min (f,g1)),( min (( max (( min (f1,g)),f)),g)))) by Th8

      .= ( min (( max (( min (f,g1)),( max (f,( min (f1,g)))))),( max (( min (f,g1)),g)))) by Th9

      .= ( min (( max (( max (f,( min (f,g1)))),( min (f1,g)))),( max (( min (f,g1)),g)))) by Th7

      .= ( min (( max (f,( min (f1,g)))),( max (( min (f,g1)),g)))) by Th8

      .= ( min (( min (( max (f,f1)),( max (f,g)))),( max (g,( min (f,g1)))))) by Th9

      .= ( min (( min (( max (f,f1)),( max (f,g)))),( min (( max (g,f)),( max (g,g1)))))) by Th9

      .= ( min (( min (( min (( max (f,f1)),( max (f,g)))),( max (g,f)))),( max (g,g1)))) by Th7

      .= ( min (( min (( max (f,f1)),( min (( max (f,g)),( max (f,g)))))),( max (g,g1)))) by Th7

      .= ( min (( max (f,g)),( min (( max (f,f1)),( max (g,g1)))))) by Th7;

      then (( max ((f \+\ g),( min (f,g)))) . x) = ( min ((( max (f,g)) . x),(( min (( max (f,f1)),( max (g,g1)))) . x))) by Def3;

      hence thesis by XXREAL_0: 17;

    end;

    theorem :: FUZZY_1:46

    (f \+\ f) = ( min (f,( 1_minus f)));

    definition

      let C be non empty set;

      let h,g be Membership_Func of C;

      :: FUZZY_1:def9

      func ab_difMF (h,g) -> Membership_Func of C means for c be Element of C holds (it . c) = |.((h . c) - (g . c)).|;

      existence

      proof

        defpred P[ object, object] means $2 = |.((h . $1) - (g . $1)).|;

        

         A1: for x,y1,y2 be object st x in C & P[x, y1] & P[x, y2] holds y1 = y2;

        

         A2: for x,y be object st x in C & P[x, y] holds y in REAL by XREAL_0:def 1;

        consider IT be PartFunc of C, REAL such that

         A3: (for x be object holds x in ( dom IT) iff x in C & ex y be object st P[x, y]) & for x be object st x in ( dom IT) holds P[x, (IT . x)] from PARTFUN1:sch 2( A2, A1);

        for x be object st x in C holds x in ( dom IT)

        proof

          let x be object;

           |.((h . x) - (g . x)).| is set by TARSKI: 1;

          hence thesis by A3;

        end;

        then C c= ( dom IT) by TARSKI:def 3;

        then

         A5: ( dom IT) = C by XBOOLE_0:def 10;

        then

         A6: for c be Element of C holds (IT . c) = |.((h . c) - (g . c)).| by A3;

        

         A7: ( rng g) c= [. 0 , 1.] by RELAT_1:def 19;

        

         A8: ( rng h) c= [. 0 , 1.] by RELAT_1:def 19;

        for y be object st y in ( rng IT) holds y in [. 0 , 1.]

        proof

          reconsider A = [. 0 , jj.] as non empty closed_interval Subset of REAL by MEASURE5: 14;

          let y be object;

          assume y in ( rng IT);

          then

          consider x be Element of C such that

           A9: x in ( dom IT) and

           A10: y = (IT . x) by PARTFUN1: 3;

           0 <= |.((h . x) - (g . x)).| by COMPLEX1: 46;

          then

           A11: 0 <= (IT . x) by A3, A9;

          

           A12: A = [.( lower_bound A), ( upper_bound A).] by INTEGRA1: 4;

          then

           A13: 0 = ( lower_bound A) by INTEGRA1: 5;

          

           A14: x in C;

          then x in ( dom h) by FUNCT_2:def 1;

          then

           A15: (h . x) in ( rng h) by FUNCT_1:def 3;

          x in ( dom g) by A14, FUNCT_2:def 1;

          then

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

          then 0 <= (g . x) by A7, A13, INTEGRA2: 1;

          then

           A17: (1 - 0 ) >= (1 - (g . x)) by XREAL_1: 10;

          

           A18: 1 = ( upper_bound A) by A12, INTEGRA1: 5;

          then (g . x) <= 1 by A7, A16, INTEGRA2: 1;

          then

           A19: ( - (g . x)) >= ( - 1) by XREAL_1: 24;

           0 <= (h . x) by A8, A13, A15, INTEGRA2: 1;

          then ( 0 - (g . x)) <= ((h . x) - (g . x)) by XREAL_1: 9;

          then

           A20: ( - 1) <= ((h . x) - (g . x)) by A19, XXREAL_0: 2;

          (h . x) <= 1 by A8, A18, A15, INTEGRA2: 1;

          then ((h . x) - (g . x)) <= (1 - (g . x)) by XREAL_1: 9;

          then ((h . x) - (g . x)) <= 1 by A17, XXREAL_0: 2;

          then |.((h . x) - (g . x)).| <= 1 by A20, ABSVALUE: 5;

          then (IT . x) <= 1 by A3, A9;

          hence thesis by A10, A13, A18, A11, INTEGRA2: 1;

        end;

        then

         A21: ( rng IT) c= [. 0 , 1.] by TARSKI:def 3;

        IT is total by A5, PARTFUN1:def 2;

        then IT is Membership_Func of C by A21, RELAT_1:def 19;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let F,G be Membership_Func of C;

        assume that

         A22: for c be Element of C holds (F . c) = |.((h . c) - (g . c)).| and

         A23: for c be Element of C holds (G . c) = |.((h . c) - (g . c)).|;

        

         A24: for c be Element of C st c in C holds (F . c) = (G . c)

        proof

          let c be Element of C;

          (F . c) = |.((h . c) - (g . c)).| by A22;

          hence thesis by A23;

        end;

        C = ( dom F) & C = ( dom G) by FUNCT_2:def 1;

        hence thesis by A24, PARTFUN1: 5;

      end;

    end