fuzzy_2.miz



    begin

    reserve x,y,y1,y2 for set;

    reserve C for non empty set;

    reserve c for Element of C;

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

    theorem :: FUZZY_2:1

    

     Th1: for x be Element of C, h be Membership_Func of C holds 0 <= (h . x) & (h . x) <= 1

    proof

      let x be Element of C, h be Membership_Func of C;

      (( EMF C) . x) = 0 by FUNCT_3:def 3;

      hence 0 <= (h . x) by FUZZY_1: 16;

      (( UMF C) . x) = 1 by FUNCT_3:def 3;

      hence thesis by FUZZY_1: 16;

    end;

    theorem :: FUZZY_2:2

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

    proof

      assume

       A1: f c= h;

      

      thus ( max (f,( min (g,h)))) = ( min (( max (f,g)),( max (f,h)))) by FUZZY_1: 9

      .= ( min (( max (f,g)),h)) by A1, FUZZY_1: 22;

    end;

    definition

      let C be non empty set;

      let f,g be Membership_Func of C;

      :: FUZZY_2:def1

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

      correctness ;

    end

    theorem :: FUZZY_2:3

    ( 1_minus (f \ g)) = ( max (( 1_minus f),g))

    proof

      

      thus ( 1_minus (f \ g)) = ( max (( 1_minus f),( 1_minus ( 1_minus g)))) by FUZZY_1: 11

      .= ( max (( 1_minus f),g));

    end;

    theorem :: FUZZY_2:4

    

     Th4: f c= g implies (f \ h) c= (g \ h)

    proof

      assume

       A1: (f . c) <= (g . c);

      let c;

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

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

      then ((f \ h) . c) <= ( min ((g . c),(( 1_minus h) . c))) by FUZZY_1: 5;

      hence thesis by FUZZY_1: 5;

    end;

    theorem :: FUZZY_2:5

    f c= g implies (h \ g) c= (h \ f)

    proof

      assume

       A1: (f . c) <= (g . c);

      let c;

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

      then (1 - (f . c)) >= (1 - (g . c)) by XREAL_1: 10;

      then (( 1_minus g) . c) <= (1 - (f . c)) by FUZZY_1:def 5;

      then (( 1_minus g) . c) <= (( 1_minus f) . c) by FUZZY_1:def 5;

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

      then ((h \ g) . c) <= ( min ((( 1_minus f) . c),(h . c))) by FUZZY_1: 5;

      hence thesis by FUZZY_1: 5;

    end;

    theorem :: FUZZY_2:6

    f c= g & h c= h1 implies (f \ h1) c= (g \ h)

    proof

      assume that

       A1: (f . c) <= (g . c) and

       A2: (h . c) <= (h1 . c);

      let c;

      (h . c) <= (h1 . c) by A2;

      then

       A3: (1 - (h . c)) >= (1 - (h1 . c)) by XREAL_1: 10;

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

      then ( min ((f . c),(1 - (h1 . c)))) <= ( min ((g . c),(1 - (h . c)))) by A3, XXREAL_0: 18;

      then ( min ((f . c),(( 1_minus h1) . c))) <= ( min ((g . c),(1 - (h . c)))) by FUZZY_1:def 5;

      then ( min ((f . c),(( 1_minus h1) . c))) <= ( min ((g . c),(( 1_minus h) . c))) by FUZZY_1:def 5;

      then (( min (f,( 1_minus h1))) . c) <= ( min ((g . c),(( 1_minus h) . c))) by FUZZY_1: 5;

      hence thesis by FUZZY_1: 5;

    end;

    theorem :: FUZZY_2:7

    (f \ ( EMF C)) = f

    proof

      

      thus (f \ ( EMF C)) = ( min (f,( UMF C))) by FUZZY_1: 40

      .= f by FUZZY_1: 18;

    end;

    theorem :: FUZZY_2:8

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

    proof

      (f \ ( min (f,g))) = ( min (f,( max (( 1_minus f),( 1_minus g))))) by FUZZY_1: 11

      .= ( max (( min (f,( 1_minus f))),(f \ g))) by FUZZY_1: 9;

      hence thesis by FUZZY_1: 17;

    end;

    theorem :: FUZZY_2:9

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

    proof

      

       A1: (f \ g) c= f by FUZZY_1: 17;

      ( min (f,g)) c= f by FUZZY_1: 17;

      hence thesis by A1, FUZZY_1: 19;

    end;

    theorem :: FUZZY_2:10

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

    proof

      ( max (f,(g \ f))) = ( min (( max (f,g)),( max (f,( 1_minus f))))) by FUZZY_1: 9;

      hence thesis by FUZZY_1: 17;

    end;

    theorem :: FUZZY_2:11

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

    proof

      (f \ (g \ h)) = ( min (f,( max (( 1_minus g),( 1_minus ( 1_minus h)))))) by FUZZY_1: 11

      .= ( max (( min (f,( 1_minus g))),( min (f,h)))) by FUZZY_1: 9;

      hence thesis;

    end;

    theorem :: FUZZY_2:12

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

    proof

      (f \ (f \ g)) = ( min (f,( max (( 1_minus f),( 1_minus ( 1_minus g)))))) by FUZZY_1: 11

      .= ( max (( min (f,( 1_minus f))),( min (f,g)))) by FUZZY_1: 9;

      hence thesis by FUZZY_1: 17;

    end;

    theorem :: FUZZY_2:13

    (f \ g) c= (( max (f,g)) \ g) by Th4, FUZZY_1: 17;

    theorem :: FUZZY_2:14

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

    proof

      

      thus (f \ ( max (g,h))) = ( min (( min (f,f)),( min (( 1_minus g),( 1_minus h))))) by FUZZY_1: 11

      .= ( min (f,( min (f,( min (( 1_minus g),( 1_minus h))))))) by FUZZY_1: 7

      .= ( min (f,( min (( min (f,( 1_minus g))),( 1_minus h))))) by FUZZY_1: 7

      .= ( min ((f \ g),(f \ h))) by FUZZY_1: 7;

    end;

    theorem :: FUZZY_2:15

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

    proof

      

      thus (f \ ( min (g,h))) = ( min (f,( max (( 1_minus g),( 1_minus h))))) by FUZZY_1: 11

      .= ( max ((f \ g),(f \ h))) by FUZZY_1: 9;

    end;

    theorem :: FUZZY_2:16

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

    proof

      

      thus ((f \ g) \ h) = ( min (f,( min (( 1_minus g),( 1_minus h))))) by FUZZY_1: 7

      .= (f \ ( max (g,h))) by FUZZY_1: 11;

    end;

    theorem :: FUZZY_2:17

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

    proof

      let c;

      ((( max (f,g)) \ ( min (f,g))) . c) = (( min (( max (f,g)),( max (( 1_minus f),( 1_minus g))))) . c) by FUZZY_1: 11

      .= (( max (( min (( max (f,g)),( 1_minus f))),( min (( max (f,g)),( 1_minus g))))) . c) by FUZZY_1: 9

      .= (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus f),g)))),( min (( 1_minus g),( max (f,g)))))) . c) by FUZZY_1: 9

      .= (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus f),g)))),( max (( min (( 1_minus g),f)),( min (( 1_minus g),g)))))) . c) by FUZZY_1: 9

      .= (( max (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus f),g)))),( min (( 1_minus g),f)))),( min (( 1_minus g),g)))) . c) by FUZZY_1: 7

      .= (( max (( max (( min (( 1_minus f),f)),( max (( min (( 1_minus f),g)),( min (( 1_minus g),f)))))),( min (( 1_minus g),g)))) . c) by FUZZY_1: 7

      .= (( max (( max (( min (( 1_minus f),g)),( min (( 1_minus g),f)))),( max (( min (( 1_minus f),f)),( min (( 1_minus g),g)))))) . c) by FUZZY_1: 7

      .= ( max (((f \+\ g) . c),(( max (( min (( 1_minus f),f)),( min (( 1_minus g),g)))) . c))) by FUZZY_1: 5;

      hence thesis by XXREAL_0: 25;

    end;

    theorem :: FUZZY_2:18

    (f \ g) c= h & (g \ f) c= h implies (f \+\ g) c= h

    proof

      assume that

       A1: ((f \ g) . c) <= (h . c) and

       A2: ((g \ f) . c) <= (h . c);

      let c;

      

       A3: (( min (g,( 1_minus f))) . c) <= (h . c) by A2;

      (( min (f,( 1_minus g))) . c) <= (h . c) by A1;

      then ( max ((( min (f,( 1_minus g))) . c),(( min (g,( 1_minus f))) . c))) <= ( max ((h . c),(h . c))) by A3, XXREAL_0: 26;

      hence thesis by FUZZY_1: 5;

    end;

    theorem :: FUZZY_2:19

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

    proof

      let c;

      (( 1_minus h) . c) <= ( max ((( 1_minus f) . c),(( 1_minus h) . c))) by XXREAL_0: 25;

      then ( min ((( min (f,g)) . c),(( 1_minus h) . c))) <= ( min ((( min (f,g)) . c),( max ((( 1_minus f) . c),(( 1_minus h) . c))))) by XXREAL_0: 18;

      then ( min ((( min (f,g)) . c),(( 1_minus h) . c))) <= ( min ((( min (f,g)) . c),(( max (( 1_minus f),( 1_minus h))) . c))) by FUZZY_1: 5;

      then

       A1: ( min ((( min (f,g)) . c),(( 1_minus h) . c))) <= (( min (( min (f,g)),( max (( 1_minus f),( 1_minus h))))) . c) by FUZZY_1: 5;

      (( min (f,(g \ h))) . c) = (( min (( min (f,g)),( 1_minus h))) . c) by FUZZY_1: 7

      .= ( min ((( min (f,g)) . c),(( 1_minus h) . c))) by FUZZY_1: 5;

      hence thesis by A1, FUZZY_1: 11;

    end;

    theorem :: FUZZY_2:20

    

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

    proof

      let c;

      ((( max (f,g)) \ ( min (f,g))) . c) = (( min (( max (f,g)),( max (( 1_minus f),( 1_minus g))))) . c) by FUZZY_1: 11

      .= (( max (( min (( max (f,g)),( 1_minus f))),( min (( max (f,g)),( 1_minus g))))) . c) by FUZZY_1: 9

      .= (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus f),g)))),( min (( 1_minus g),( max (f,g)))))) . c) by FUZZY_1: 9

      .= (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus f),g)))),( max (( min (( 1_minus g),f)),( min (( 1_minus g),g)))))) . c) by FUZZY_1: 9

      .= (( max (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus f),g)))),( min (( 1_minus g),g)))),( min (( 1_minus g),f)))) . c) by FUZZY_1: 7

      .= (( max (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus g),g)))),( min (( 1_minus f),g)))),( min (( 1_minus g),f)))) . c) by FUZZY_1: 7

      .= (( max (( max (( min (( 1_minus f),f)),( min (( 1_minus g),g)))),( max (( min (( 1_minus f),g)),( min (( 1_minus g),f)))))) . c) by FUZZY_1: 7

      .= ( max ((( max (( min (( 1_minus f),f)),( min (( 1_minus g),g)))) . c),((f \+\ g) . c))) by FUZZY_1: 5;

      hence thesis by XXREAL_0: 25;

    end;

    theorem :: FUZZY_2:21

    

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

    proof

      (f \+\ g) c= (( max (f,g)) \ ( min (f,g))) by Th20;

      then ( 1_minus (( max (f,g)) \ ( min (f,g)))) c= ( 1_minus (f \+\ g)) by FUZZY_1: 36;

      then ( max (( 1_minus ( max (f,g))),( 1_minus ( 1_minus ( min (f,g)))))) c= ( 1_minus (f \+\ g)) by FUZZY_1: 11;

      hence thesis;

    end;

    theorem :: FUZZY_2:22

    ((f \+\ g) \ h) = ( max ((f \ ( max (g,h))),(g \ ( max (f,h)))))

    proof

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

      (( max (( min (f,g1)),( min (f1,g)))) \ h) = ( max (( min (h1,( min (f,g1)))),( min (h1,( min (f1,g)))))) by FUZZY_1: 9

      .= ( max (( min (( min (h1,g1)),f)),( min (h1,( min (f1,g)))))) by FUZZY_1: 7

      .= ( max (( min (( min (h1,g1)),f)),( min (( min (h1,f1)),g)))) by FUZZY_1: 7

      .= ( max (( min (f,( 1_minus ( max (h,g))))),( min (g,( min (h1,f1)))))) by FUZZY_1: 11

      .= ( max ((f \ ( max (h,g))),(g \ ( max (f,h))))) by FUZZY_1: 11;

      hence thesis;

    end;

    theorem :: FUZZY_2:23

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

    proof

      ( max ((f \ ( max (g,h))),( min (( min (f,g)),h)))) = ( max (( min (f,( 1_minus ( max (g,h))))),( min (f,( min (g,h)))))) by FUZZY_1: 7

      .= ( min (f,( max (( 1_minus ( max (g,h))),( min (g,h)))))) by FUZZY_1: 9;

      hence thesis by Th21, FUZZY_1: 25;

    end;

    theorem :: FUZZY_2:24

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

    proof

      assume

       A1: (f . c) <= (g . c);

      let c;

      

       A2: (f . c) <= (g . c) by A1;

      (( max (f,(g \ f))) . c) = (( min (( max (f,g)),( max (f,( 1_minus f))))) . c) by FUZZY_1: 9

      .= ( min ((( max (f,g)) . c),(( max (f,( 1_minus f))) . c))) by FUZZY_1: 5

      .= ( min (( max ((f . c),(g . c))),(( max (f,( 1_minus f))) . c))) by FUZZY_1: 5

      .= ( min ((g . c),(( max (f,( 1_minus f))) . c))) by A2, XXREAL_0:def 10;

      hence thesis by XXREAL_0: 17;

    end;

    theorem :: FUZZY_2:25

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

    proof

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

      let c;

      ( max ((f \+\ g),( min (f,g)))) = ( max (( min (f,g1)),( max (( min (f1,g)),( min (f,g)))))) by FUZZY_1: 7

      .= ( max (( min (f,g1)),( min (( max (( min (f1,g)),f)),( max (( min (f1,g)),g)))))) by FUZZY_1: 9

      .= ( max (( min (f,g1)),( min (( max (( min (f1,g)),f)),g)))) by FUZZY_1: 8

      .= ( min (( max (( min (f,g1)),( max (( min (f1,g)),f)))),( max (( min (f,g1)),g)))) by FUZZY_1: 9;

      then (( max ((f \+\ g),( min (f,g)))) . c) = ( min ((( max (( min (f,g1)),( max (( min (f1,g)),f)))) . c),(( max (( min (f,g1)),g)) . c))) by FUZZY_1: 5;

      then

       A1: (( max ((f \+\ g),( min (f,g)))) . c) <= (( max (( min (f,g1)),g)) . c) by XXREAL_0: 17;

      (( max (( min (f,g1)),g)) . c) = (( min (( max (g,f)),( max (g,g1)))) . c) by FUZZY_1: 9

      .= ( min ((( max (f,g)) . c),(( max (g,g1)) . c))) by FUZZY_1: 5;

      then (( max (( min (f,g1)),g)) . c) <= (( max (f,g)) . c) by XXREAL_0: 17;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: FUZZY_2:26

    

     Th26: (f \ g) = ( EMF C) implies f c= g

    proof

      assume

       A1: (f \ g) = ( EMF C);

      let c;

      

       A2: ( min ((f . c),(( 1_minus g) . c))) = (( EMF C) . c) by A1, FUZZY_1: 5;

      per cases by A2, XXREAL_0: 15;

        suppose (f . c) = (( EMF C) . c);

        hence thesis by FUZZY_1: 16;

      end;

        suppose

         A3: (( 1_minus g) . c) = (( EMF C) . c);

        (g . c) = (( 1_minus ( 1_minus g)) . c)

        .= (1 - (( 1_minus g) . c)) by FUZZY_1:def 5

        .= (( 1_minus ( EMF C)) . c) by A3, FUZZY_1:def 5

        .= (( UMF C) . c) by FUZZY_1: 40;

        hence thesis by FUZZY_1: 16;

      end;

    end;

    theorem :: FUZZY_2:27

    

     Th27: ( min (f,g)) = ( EMF C) implies (f \ g) = f

    proof

      

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

      assume

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

      

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

      proof

        let x be Element of C;

        

         A4: (( EMF C) . x) = ( min ((f . x),(g . x))) by A2, FUZZY_1: 5;

        per cases by A4, XXREAL_0: 15;

          suppose

           A5: (f . x) = (( EMF C) . x);

          (( min (f,( 1_minus g))) . x) = ( min ((f . x),(( 1_minus g) . x))) by FUZZY_1: 5

          .= (( min (( 1_minus g),( EMF C))) . x) by A5, FUZZY_1: 5

          .= (( EMF C) . x) by FUZZY_1: 18;

          hence thesis by A5;

        end;

          suppose

           A6: (g . x) = (( EMF C) . x);

          (( min (f,( 1_minus g))) . x) = ( min ((f . x),(( 1_minus g) . x))) by FUZZY_1: 5

          .= ( min ((f . x),(1 - (( EMF C) . x)))) by A6, FUZZY_1:def 5

          .= ( min ((f . x),(( 1_minus ( EMF C)) . x))) by FUZZY_1:def 5

          .= ( min ((f . x),(( UMF C) . x))) by FUZZY_1: 40

          .= (( min (f,( UMF C))) . x) by FUZZY_1: 5;

          hence thesis by FUZZY_1: 18;

        end;

      end;

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

      hence thesis by A1, A3, PARTFUN1: 5;

    end;

    begin

    reconsider jj = 1 as Real;

    definition

      let C be non empty set;

      let h,g be Membership_Func of C;

      :: FUZZY_2:def2

      func h * g -> Membership_Func of C means

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

          

           A4: ex y st y = ((h . x) * (g . x));

          assume x in C;

          hence thesis by A3, A4;

        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;

          

           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

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

          

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

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

          then

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

          then

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

           0 <= (g . x) by A7, A12, A17, INTEGRA2: 1;

          then 0 <= ((h . x) * (g . x)) by A15, XREAL_1: 127;

          then

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

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

          then ((h . x) * (g . x)) <= 1 by A15, A18, XREAL_1: 160;

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

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

        end;

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

        then IT is Membership_Func of C by A5, FUNCT_2:def 1, 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) = ((h . c) * (g . c)) and

         A21: for c be Element of C holds (G . c) = ((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) = ((h . c) * (g . c)) by A20;

          hence thesis by A21;

        end;

        

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

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

        hence thesis by A23, A22, PARTFUN1: 5;

      end;

      commutativity ;

    end

    definition

      let C be non empty set;

      let h,g be Membership_Func of C;

      :: FUZZY_2:def3

      func h ++ g -> Membership_Func of C means

      : Def3: for c be Element of C holds (it . c) = (((h . c) + (g . c)) - ((h . c) * (g . c)));

      existence

      proof

        defpred P[ object, object] means $2 = (((h . $1) + (g . $1)) - ((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;

          

           A4: ex y st y = (((h . x) + (g . x)) - ((h . x) * (g . x)));

          assume x in C;

          hence thesis by A3, A4;

        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)) - ((h . c) * (g . c))) by A3;

        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

           A7: x in ( dom IT) and

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

           0 <= (( 1_minus h) . x) by Th1;

          then

           A9: 0 <= (1 - (h . x)) by FUZZY_1:def 5;

          (( 1_minus g) . x) <= 1 by Th1;

          then

           A10: (1 - (g . x)) <= 1 by FUZZY_1:def 5;

          (( 1_minus h) . x) <= 1 by Th1;

          then (1 - (h . x)) <= 1 by FUZZY_1:def 5;

          then ((1 - (h . x)) * (1 - (g . x))) <= 1 by A9, A10, XREAL_1: 160;

          then (1 - ((1 - (h . x)) * (1 - (g . x)))) >= (1 - 1) by XREAL_1: 10;

          then 0 <= (((h . x) + (g . x)) - ((h . x) * (g . x)));

          then

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

          

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

          then

           A13: 1 = ( upper_bound A) by INTEGRA1: 5;

           0 <= (( 1_minus g) . x) by Th1;

          then 0 <= (1 - (g . x)) by FUZZY_1:def 5;

          then 0 <= ((1 - (h . x)) * (1 - (g . x))) by A9, XREAL_1: 127;

          then (1 - 0 ) >= (1 - ((1 - (h . x)) * (1 - (g . x)))) by XREAL_1: 10;

          then (((h . x) + (g . x)) - ((h . x) * (g . x))) <= 1;

          then

           A14: (IT . x) <= 1 by A3, A7;

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

          hence thesis by A8, A13, A11, A14, INTEGRA2: 1;

        end;

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

        then IT is Membership_Func of C by A5, FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let F,G be Membership_Func of C;

        assume that

         A15: for c be Element of C holds (F . c) = (((h . c) + (g . c)) - ((h . c) * (g . c))) and

         A16: for c be Element of C holds (G . c) = (((h . c) + (g . c)) - ((h . c) * (g . c)));

        

         A17: 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)) - ((h . c) * (g . c))) by A15;

          hence thesis by A16;

        end;

        

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

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

        hence thesis by A18, A17, PARTFUN1: 5;

      end;

      commutativity ;

    end

    theorem :: FUZZY_2:28

    

     Th28: (f * f) c= f & f c= (f ++ f)

    proof

      thus (f * f) c= f

      proof

        let c;

        

         A1: 0 <= (f . c) by Th1;

        (f . c) <= 1 by Th1;

        then ((f . c) * (f . c)) <= (1 * (f . c)) by A1, XREAL_1: 64;

        hence thesis by Def2;

      end;

      let c;

      

       A2: 0 <= (f . c) by Th1;

       0 <= (( 1_minus f) . c) by Th1;

      then ( 0 * (f . c)) <= ((f . c) * (( 1_minus f) . c)) by A2, XREAL_1: 64;

      then 0 <= ((f . c) * (1 - (f . c))) by FUZZY_1:def 5;

      then ( 0 + (f . c)) <= (((f . c) - ((f . c) * (f . c))) + (f . c)) by XREAL_1: 6;

      then (f . c) <= (((f . c) + (f . c)) - ((f . c) * (f . c)));

      hence thesis by Def3;

    end;

    theorem :: FUZZY_2:29

    

     Th29: ((f * g) * h) = (f * (g * h))

    proof

      

       A1: C = ( dom (f * (g * h))) by FUNCT_2:def 1;

      

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

      proof

        let c;

        (((f * g) * h) . c) = (((f * g) . c) * (h . c)) by Def2

        .= (((f . c) * (g . c)) * (h . c)) by Def2

        .= ((f . c) * ((g . c) * (h . c)))

        .= ((f . c) * ((g * h) . c)) by Def2;

        hence thesis by Def2;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:30

    ((f ++ g) ++ h) = (f ++ (g ++ h))

    proof

      

       A1: C = ( dom (f ++ (g ++ h))) by FUNCT_2:def 1;

      

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

      proof

        let c;

        set x = (f . c), y = (g . c), z = (h . c);

        

         A3: ((f ++ (g ++ h)) . c) = ((x + ((g ++ h) . c)) - (x * ((g ++ h) . c))) by Def3

        .= ((x + ((y + z) - (y * z))) - (x * ((g ++ h) . c))) by Def3

        .= (((x + (y + z)) - (y * z)) - (x * ((y + z) - (y * z)))) by Def3

        .= ((((( - (y * z)) - (x * y)) - (x * z)) + ((x * y) * z)) + ((x + y) + z));

        (((f ++ g) ++ h) . c) = ((((f ++ g) . c) + (h . c)) - (((f ++ g) . c) * (h . c))) by Def3

        .= (((((f . c) + (g . c)) - ((f . c) * (g . c))) + (h . c)) - (((f ++ g) . c) * (h . c))) by Def3

        .= (((( - (x * y)) + (x + y)) + z) - (((x + y) - (x * y)) * z)) by Def3

        .= ((((( - (x * y)) - (x * z)) - (y * z)) + ((x * y) * z)) + ((x + y) + z));

        hence thesis by A3;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:31

    (f * (f ++ g)) c= f & f c= (f ++ (f * g))

    proof

      thus (f * (f ++ g)) c= f

      proof

        let c;

        

         A1: ((f ++ g) . c) <= 1 by Th1;

         0 <= (f . c) by Th1;

        then (((f ++ g) . c) * (f . c)) <= (1 * (f . c)) by A1, XREAL_1: 64;

        hence thesis by Def2;

      end;

      let c;

      

       A2: (( 1_minus f) . c) >= 0 by Th1;

      ((f * g) . c) >= 0 by Th1;

      then ( 0 * ((f * g) . c)) <= ((( 1_minus f) . c) * ((f * g) . c)) by A2, XREAL_1: 64;

      then 0 <= ((1 - (f . c)) * ((f * g) . c)) by FUZZY_1:def 5;

      then ( 0 + (f . c)) <= ((((f * g) . c) - ((f . c) * ((f * g) . c))) + (f . c)) by XREAL_1: 6;

      then (f . c) <= (((f . c) + ((f * g) . c)) - ((f . c) * ((f * g) . c)));

      hence thesis by Def3;

    end;

    theorem :: FUZZY_2:32

    (f * (g ++ h)) c= ((f * g) ++ (f * h))

    proof

      let c;

      set x = (f . c), y = (g . c), z = (h . c);

      (f * f) c= f by Th28;

      then

       A1: ((f * f) . c) <= (f . c);

      ((g * h) . c) >= 0 by Th1;

      then (((f * f) . c) * ((g * h) . c)) <= ((f . c) * ((g * h) . c)) by A1, XREAL_1: 64;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * f) . c) * ((g * h) . c))) >= ((((f * g) . c) + ((f * h) . c)) - ((f . c) * ((g * h) . c))) by XREAL_1: 10;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c)) >= ((((f * g) . c) + ((f * h) . c)) - ((f . c) * ((g * h) . c))) by Def2;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c)) >= (((x * y) + ((f * h) . c)) - ((f . c) * ((g * h) . c))) by Def2;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c)) >= (((x * y) + (x * z)) - ((f . c) * ((g * h) . c))) by Def2;

      then ((((f * g) . c) + ((f * h) . c)) - ((f * (f * (g * h))) . c)) >= (((x * y) + (x * z)) - ((f . c) * ((g * h) . c))) by Th29;

      then ((((f * g) . c) + ((f * h) . c)) - ((f * ((g * f) * h)) . c)) >= (((y + z) - ((g * h) . c)) * x) by Th29;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * g) * (f * h)) . c)) >= (((y + z) - ((g * h) . c)) * x) by Th29;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * g) * (f * h)) . c)) >= (x * ((y + z) - (y * z))) by Def2;

      then ((((f * g) . c) + ((f * h) . c)) - (((f * g) . c) * ((f * h) . c))) >= (x * ((y + z) - (y * z))) by Def2;

      then (((f * g) ++ (f * h)) . c) >= (x * ((y + z) - (y * z))) by Def3;

      then (((f * g) ++ (f * h)) . c) >= (x * ((g ++ h) . c)) by Def3;

      hence thesis by Def2;

    end;

    theorem :: FUZZY_2:33

    ((f ++ g) * (f ++ h)) c= (f ++ (g * h))

    proof

      let c;

      set x = (f . c), y = (g . c), z = (h . c);

      (f * f) c= f by Th28;

      then ((f * f) . c) <= (f . c);

      then (x * x) <= x by Def2;

      then

       A1: ((x * x) - x) <= 0 by XREAL_1: 47;

       0 <= (( 1_minus (g ++ h)) . c) by Th1;

      then

       A2: ((( 1_minus (g ++ h)) . c) * (( - x) + (x * x))) <= ( 0 * (( - x) + (x * x))) by A1, XREAL_1: 65;

      ((((f ++ g) * (f ++ h)) . c) - ((f ++ (g * h)) . c)) = ((((f ++ g) . c) * ((f ++ h) . c)) - ((f ++ (g * h)) . c)) by Def2

      .= ((((x + y) - (x * y)) * ((f ++ h) . c)) - ((f ++ (g * h)) . c)) by Def3

      .= ((((x + y) - (x * y)) * ((x + z) - (x * z))) - ((f ++ (g * h)) . c)) by Def3

      .= ((((x + y) - (x * y)) * ((x + z) - (x * z))) - ((x + ((g * h) . c)) - (x * ((g * h) . c)))) by Def3

      .= ((((x + y) - (x * y)) * ((x + z) - (x * z))) - ((x + (y * z)) - (x * ((g * h) . c)))) by Def2

      .= ((((x - (x * y)) + y) * ((x + z) - (x * z))) - ((x + (y * z)) - ((y * z) * x))) by Def2

      .= ((x * (((y + z) - (y * z)) - 1)) + ((((( - y) + (y * z)) - z) + 1) * (x * x)))

      .= ((x * (((g ++ h) . c) - 1)) + ((( - ((y + z) - (y * z))) + 1) * (x * x))) by Def3

      .= ((x * ( - (( - ((g ++ h) . c)) + 1))) + ((( - ((g ++ h) . c)) + 1) * (x * x))) by Def3

      .= ((1 - ((g ++ h) . c)) * (( - x) + (x * x)))

      .= ((( 1_minus (g ++ h)) . c) * (( - x) + (x * x))) by FUZZY_1:def 5;

      hence thesis by A2, XREAL_1: 50;

    end;

    theorem :: FUZZY_2:34

    ( 1_minus (f * g)) = (( 1_minus f) ++ ( 1_minus g))

    proof

      

       A1: C = ( dom (( 1_minus f) ++ ( 1_minus g))) by FUNCT_2:def 1;

      

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

      proof

        let c;

        ((( 1_minus f) ++ ( 1_minus g)) . c) = (((( 1_minus f) . c) + (( 1_minus g) . c)) - ((( 1_minus f) . c) * (( 1_minus g) . c))) by Def3

        .= (((1 - (f . c)) + (( 1_minus g) . c)) - ((( 1_minus f) . c) * (( 1_minus g) . c))) by FUZZY_1:def 5

        .= (((1 - (f . c)) + (1 - (g . c))) - ((( 1_minus f) . c) * (( 1_minus g) . c))) by FUZZY_1:def 5

        .= (((1 - (f . c)) + (1 - (g . c))) - ((1 - (f . c)) * (( 1_minus g) . c))) by FUZZY_1:def 5

        .= (((1 - (f . c)) + (1 - (g . c))) - ((1 - (f . c)) * (1 - (g . c)))) by FUZZY_1:def 5

        .= ((((g . c) - (g . c)) + 1) - ((f . c) * (g . c)))

        .= (1 - ((f * g) . c)) by Def2;

        hence thesis by FUZZY_1:def 5;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:35

    ( 1_minus (f ++ g)) = (( 1_minus f) * ( 1_minus g))

    proof

      

       A1: C = ( dom (( 1_minus f) * ( 1_minus g))) by FUNCT_2:def 1;

      

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

      proof

        let c;

        ((( 1_minus f) * ( 1_minus g)) . c) = ((( 1_minus f) . c) * (( 1_minus g) . c)) by Def2

        .= ((1 - (f . c)) * (( 1_minus g) . c)) by FUZZY_1:def 5

        .= ((1 - (f . c)) * (1 - (g . c))) by FUZZY_1:def 5

        .= (1 - (((f . c) + (g . c)) - ((f . c) * (g . c))))

        .= (1 - ((f ++ g) . c)) by Def3;

        hence thesis by FUZZY_1:def 5;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:36

    

     Th36: (f ++ g) = ( 1_minus (( 1_minus f) * ( 1_minus g)))

    proof

      

       A1: C = ( dom ( 1_minus (( 1_minus f) * ( 1_minus g)))) by FUNCT_2:def 1;

      

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

      proof

        let c;

        (( 1_minus (( 1_minus f) * ( 1_minus g))) . c) = (1 - ((( 1_minus f) * ( 1_minus g)) . c)) by FUZZY_1:def 5

        .= (1 - ((( 1_minus f) . c) * (( 1_minus g) . c))) by Def2

        .= (1 - ((1 - (f . c)) * (( 1_minus g) . c))) by FUZZY_1:def 5

        .= (1 - ((1 - (f . c)) * (1 - (g . c)))) by FUZZY_1:def 5

        .= (((f . c) + (g . c)) - ((f . c) * (g . c)));

        hence thesis by Def3;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:37

    (f * ( EMF C)) = ( EMF C) & (f * ( UMF C)) = f

    proof

      

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

      

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

      

       A3: for c be Element of C st c in C holds ((f * ( UMF C)) . c) = (f . c)

      proof

        let c;

        ((f * ( UMF C)) . c) = ((f . c) * (( UMF C) . c)) by Def2

        .= ((f . c) * 1) by FUNCT_3:def 3;

        hence thesis;

      end;

      

       A4: for c be Element of C st c in C holds ((f * ( EMF C)) . c) = (( EMF C) . c)

      proof

        let c;

        ((f * ( EMF C)) . c) = ((f . c) * (( EMF C) . c)) by Def2

        .= ((f . c) * 0 ) by FUNCT_3:def 3;

        hence thesis by FUNCT_3:def 3;

      end;

      

       A5: C = ( dom (f * ( UMF C))) by FUNCT_2:def 1;

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

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

    end;

    theorem :: FUZZY_2:38

    (f ++ ( EMF C)) = f & (f ++ ( UMF C)) = ( UMF C)

    proof

      

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

      

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

      

       A3: for c be Element of C st c in C holds ((f ++ ( UMF C)) . c) = (( UMF C) . c)

      proof

        let c;

        ((f ++ ( UMF C)) . c) = (((f . c) + (( UMF C) . c)) - ((f . c) * (( UMF C) . c))) by Def3

        .= (((( UMF C) . c) + (f . c)) - ((f . c) * 1)) by FUNCT_3:def 3

        .= ((( UMF C) . c) + ((f . c) - (f . c)));

        hence thesis;

      end;

      

       A4: for c be Element of C st c in C holds ((f ++ ( EMF C)) . c) = (f . c)

      proof

        let c;

        ((f ++ ( EMF C)) . c) = (((f . c) + (( EMF C) . c)) - ((f . c) * (( EMF C) . c))) by Def3

        .= (((f . c) + 0 ) - ((f . c) * (( EMF C) . c))) by FUNCT_3:def 3

        .= ((f . c) - ((f . c) * 0 )) by FUNCT_3:def 3;

        hence thesis;

      end;

      

       A5: C = ( dom (f ++ ( UMF C))) by FUNCT_2:def 1;

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

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

    end;

    theorem :: FUZZY_2:39

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

    proof

      let c;

      

       A1: (( min (f,g)) . c) = ( min ((f . c),(g . c))) by FUZZY_1: 5;

      per cases by A1, XXREAL_0: 15;

        suppose

         A2: (( min (f,g)) . c) = (f . c);

        

         A3: (f . c) >= 0 by Th1;

        (g . c) <= 1 by Th1;

        then ((g . c) * (f . c)) <= (1 * (f . c)) by A3, XREAL_1: 64;

        hence thesis by A2, Def2;

      end;

        suppose

         A4: (( min (f,g)) . c) = (g . c);

        

         A5: (g . c) >= 0 by Th1;

        (f . c) <= 1 by Th1;

        then ((f . c) * (g . c)) <= (1 * (g . c)) by A5, XREAL_1: 64;

        hence thesis by A4, Def2;

      end;

    end;

    theorem :: FUZZY_2:40

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

    proof

      let c;

      

       A1: (( max (f,g)) . c) = ( max ((f . c),(g . c))) by FUZZY_1: 5;

      per cases by A1, XXREAL_0: 16;

        suppose

         A2: (( max (f,g)) . c) = (f . c);

        

         A3: (( 1_minus f) . c) >= 0 by Th1;

        (g . c) >= 0 by Th1;

        then ( 0 * (g . c)) <= ((g . c) * (( 1_minus f) . c)) by A3, XREAL_1: 64;

        then 0 <= ((g . c) * (1 - (f . c))) by FUZZY_1:def 5;

        then ( 0 + (f . c)) <= (((g . c) - ((f . c) * (g . c))) + (f . c)) by XREAL_1: 6;

        then (f . c) <= (((f . c) + (g . c)) - ((f . c) * (g . c)));

        hence thesis by A2, Def3;

      end;

        suppose

         A4: (( max (f,g)) . c) = (g . c);

        

         A5: (( 1_minus g) . c) >= 0 by Th1;

        (f . c) >= 0 by Th1;

        then ( 0 * (f . c)) <= ((f . c) * (( 1_minus g) . c)) by A5, XREAL_1: 64;

        then 0 <= ((f . c) * (1 - (g . c))) by FUZZY_1:def 5;

        then ( 0 + (g . c)) <= (((f . c) - ((f . c) * (g . c))) + (g . c)) by XREAL_1: 6;

        then (g . c) <= (((f . c) + (g . c)) - ((f . c) * (g . c)));

        hence thesis by A4, Def3;

      end;

    end;

    

     Lm1: for a,b,c be Real st 0 <= c holds (c * ( min (a,b))) = ( min ((c * a),(c * b)))

    proof

      let a,b,c be Real;

      assume

       A1: 0 <= c;

      per cases by XXREAL_0: 15;

        suppose

         A2: ( min (a,b)) = a;

        then a <= b by XXREAL_0:def 9;

        then (a * c) <= (b * c) by A1, XREAL_1: 64;

        hence thesis by A2, XXREAL_0:def 9;

      end;

        suppose

         A3: ( min (a,b)) = b;

        then a >= b by XXREAL_0:def 9;

        then (a * c) >= (b * c) by A1, XREAL_1: 64;

        hence thesis by A3, XXREAL_0:def 9;

      end;

    end;

    

     Lm2: for a,b,c be Real st 0 <= c holds (c * ( max (a,b))) = ( max ((c * a),(c * b)))

    proof

      let a,b,c be Real;

      assume

       A1: 0 <= c;

      per cases by XXREAL_0: 16;

        suppose

         A2: ( max (a,b)) = b;

        then a <= b by XXREAL_0:def 10;

        then (a * c) <= (c * b) by A1, XREAL_1: 64;

        hence thesis by A2, XXREAL_0:def 10;

      end;

        suppose

         A3: ( max (a,b)) = a;

        then a >= b by XXREAL_0:def 10;

        then (a * c) >= (b * c) by A1, XREAL_1: 64;

        hence thesis by A3, XXREAL_0:def 10;

      end;

    end;

    theorem :: FUZZY_2:41

    for a,b,c be Real st 0 <= c holds (c * ( max (a,b))) = ( max ((c * a),(c * b))) & (c * ( min (a,b))) = ( min ((c * a),(c * b))) by Lm1, Lm2;

    theorem :: FUZZY_2:42

    for a,b,c be Real holds (c + ( max (a,b))) = ( max ((c + a),(c + b))) & (c + ( min (a,b))) = ( min ((c + a),(c + b)))

    proof

      let a,b,c be Real;

      

       A1: (c + ( min (a,b))) = ( min ((c + a),(c + b)))

      proof

        per cases by XXREAL_0: 15;

          suppose

           A2: ( min (a,b)) = a;

          then a <= b by XXREAL_0:def 9;

          then (a + c) <= (c + b) by XREAL_1: 6;

          hence thesis by A2, XXREAL_0:def 9;

        end;

          suppose

           A3: ( min (a,b)) = b;

          then a >= b by XXREAL_0:def 9;

          then (a + c) >= (b + c) by XREAL_1: 6;

          hence thesis by A3, XXREAL_0:def 9;

        end;

      end;

      (c + ( max (a,b))) = ( max ((c + a),(c + b)))

      proof

        per cases by XXREAL_0: 16;

          suppose

           A4: ( max (a,b)) = b;

          then a <= b by XXREAL_0:def 10;

          then (c + a) <= (c + b) by XREAL_1: 6;

          hence thesis by A4, XXREAL_0:def 10;

        end;

          suppose

           A5: ( max (a,b)) = a;

          then a >= b by XXREAL_0:def 10;

          then (a + c) >= (b + c) by XREAL_1: 6;

          hence thesis by A5, XXREAL_0:def 10;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: FUZZY_2:43

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

    proof

      

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

      

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

      proof

        let c;

        ((f * ( max (g,h))) . c) = ((f . c) * (( max (g,h)) . c)) by Def2

        .= ((f . c) * ( max ((g . c),(h . c)))) by FUZZY_1: 5

        .= ( max (((f . c) * (g . c)),((f . c) * (h . c)))) by Lm2, Th1

        .= ( max (((f * g) . c),((f . c) * (h . c)))) by Def2

        .= ( max (((f * g) . c),((f * h) . c))) by Def2;

        hence thesis by FUZZY_1: 5;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:44

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

    proof

      

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

      

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

      proof

        let c;

        ((f * ( min (g,h))) . c) = ((f . c) * (( min (g,h)) . c)) by Def2

        .= ((f . c) * ( min ((g . c),(h . c)))) by FUZZY_1: 5

        .= ( min (((f . c) * (g . c)),((f . c) * (h . c)))) by Lm1, Th1

        .= ( min (((f * g) . c),((f . c) * (h . c)))) by Def2

        .= ( min (((f * g) . c),((f * h) . c))) by Def2;

        hence thesis by FUZZY_1: 5;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:45

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

    proof

      

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

      

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

      proof

        let c;

        

         A3: ((f ++ ( max (g,h))) . c) = (((f . c) + (( max (g,h)) . c)) - ((f . c) * (( max (g,h)) . c))) by Def3

        .= (((f . c) + ( max ((g . c),(h . c)))) - ((f . c) * (( max (g,h)) . c))) by FUZZY_1: 5;

        per cases by XXREAL_0: 16;

          suppose

           A4: ( max ((g . c),(h . c))) = (g . c);

          

           A5: (( 1_minus f) . c) >= 0 by Th1;

          (g . c) >= (h . c) by A4, XXREAL_0:def 10;

          then ((g . c) * (( 1_minus f) . c)) >= ((h . c) * (( 1_minus f) . c)) by A5, XREAL_1: 64;

          then ((g . c) * (1 - (f . c))) >= ((h . c) * (( 1_minus f) . c)) by FUZZY_1:def 5;

          then ((g . c) * (1 - (f . c))) >= ((h . c) * (1 - (f . c))) by FUZZY_1:def 5;

          then ((((g . c) * 1) - ((g . c) * (f . c))) + (f . c)) >= (((h . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

          

          then

           A6: (((f . c) + (g . c)) - ((f . c) * (g . c))) = ( max ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by XXREAL_0:def 10

          .= ( max (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by Def3

          .= ( max (((f ++ g) . c),((f ++ h) . c))) by Def3;

          ((f ++ ( max (g,h))) . c) = (((f . c) + (g . c)) - ((f . c) * (g . c))) by A3, A4, FUZZY_1: 5;

          hence thesis by A6, FUZZY_1: 5;

        end;

          suppose

           A7: ( max ((g . c),(h . c))) = (h . c);

          

           A8: (( 1_minus f) . c) >= 0 by Th1;

          (h . c) >= (g . c) by A7, XXREAL_0:def 10;

          then ((h . c) * (( 1_minus f) . c)) >= ((g . c) * (( 1_minus f) . c)) by A8, XREAL_1: 64;

          then ((h . c) * (1 - (f . c))) >= ((g . c) * (( 1_minus f) . c)) by FUZZY_1:def 5;

          then ((h . c) * (1 - (f . c))) >= ((g . c) * (1 - (f . c))) by FUZZY_1:def 5;

          then ((((h . c) * 1) - ((h . c) * (f . c))) + (f . c)) >= (((g . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

          

          then

           A9: (((f . c) + (h . c)) - ((f . c) * (h . c))) = ( max ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by XXREAL_0:def 10

          .= ( max (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by Def3

          .= ( max (((f ++ g) . c),((f ++ h) . c))) by Def3;

          ((f ++ ( max (g,h))) . c) = (((f . c) + (h . c)) - ((f . c) * (h . c))) by A3, A7, FUZZY_1: 5;

          hence thesis by A9, FUZZY_1: 5;

        end;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:46

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

    proof

      

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

      

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

      proof

        let c;

        

         A3: ((f ++ ( min (g,h))) . c) = (((f . c) + (( min (g,h)) . c)) - ((f . c) * (( min (g,h)) . c))) by Def3

        .= (((f . c) + ( min ((g . c),(h . c)))) - ((f . c) * (( min (g,h)) . c))) by FUZZY_1: 5;

        now

          per cases by XXREAL_0: 15;

            suppose

             A4: ( min ((g . c),(h . c))) = (g . c);

            

             A5: (( 1_minus f) . c) >= 0 by Th1;

            (g . c) <= (h . c) by A4, XXREAL_0:def 9;

            then ((g . c) * (( 1_minus f) . c)) <= ((h . c) * (( 1_minus f) . c)) by A5, XREAL_1: 64;

            then ((g . c) * (1 - (f . c))) <= ((h . c) * (( 1_minus f) . c)) by FUZZY_1:def 5;

            then ((g . c) * (1 - (f . c))) <= ((h . c) * (1 - (f . c))) by FUZZY_1:def 5;

            then ((((g . c) * 1) - ((g . c) * (f . c))) + (f . c)) <= (((h . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

            

            then

             A6: (((f . c) + (g . c)) - ((f . c) * (g . c))) = ( min ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by XXREAL_0:def 9

            .= ( min (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by Def3

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

            ((f ++ ( min (g,h))) . c) = (((f . c) + (g . c)) - ((f . c) * (g . c))) by A3, A4, FUZZY_1: 5;

            hence thesis by A6, FUZZY_1: 5;

          end;

            suppose

             A7: ( min ((g . c),(h . c))) = (h . c);

            

             A8: (( 1_minus f) . c) >= 0 by Th1;

            (h . c) <= (g . c) by A7, XXREAL_0:def 9;

            then ((h . c) * (( 1_minus f) . c)) <= ((g . c) * (( 1_minus f) . c)) by A8, XREAL_1: 64;

            then ((h . c) * (1 - (f . c))) <= ((g . c) * (( 1_minus f) . c)) by FUZZY_1:def 5;

            then ((h . c) * (1 - (f . c))) <= ((g . c) * (1 - (f . c))) by FUZZY_1:def 5;

            then ((((h . c) * 1) - ((h . c) * (f . c))) + (f . c)) <= (((g . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

            

            then

             A9: (((f . c) + (h . c)) - ((f . c) * (h . c))) = ( min ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by XXREAL_0:def 9

            .= ( min (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c))))) by Def3

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

            ((f ++ ( min (g,h))) . c) = (((f . c) + (h . c)) - ((f . c) * (h . c))) by A3, A7, FUZZY_1: 5;

            hence thesis by A9, FUZZY_1: 5;

          end;

        end;

        hence thesis;

      end;

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

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_2:47

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

    proof

      let c;

      

       A1: (( max ((f . c),(g . c))) * ( max ((f . c),(h . c)))) <= (( max (f,(g * h))) . c)

      proof

        per cases by XXREAL_0: 16;

          suppose

           A2: ( max ((f . c),(g . c))) = (f . c);

          (( max ((f . c),(g . c))) * ( max ((f . c),(h . c)))) <= (( max (f,(g * h))) . c)

          proof

            per cases by XXREAL_0: 16;

              suppose

               A3: ( max ((f . c),(h . c))) = (f . c);

              (( max (f,(g * h))) . c) = ( max ((f . c),((g * h) . c))) by FUZZY_1: 5;

              then

               A4: (( max (f,(g * h))) . c) >= (f . c) by XXREAL_0: 25;

              (f * f) c= f by Th28;

              then ((f * f) . c) <= (f . c);

              then ((f * f) . c) <= (( max (f,(g * h))) . c) by A4, XXREAL_0: 2;

              hence thesis by A2, A3, Def2;

            end;

              suppose

               A5: ( max ((f . c),(h . c))) = (h . c);

              

               A6: 1 >= (h . c) by Th1;

              (f . c) <= ( max ((f . c),((g * h) . c))) by XXREAL_0: 25;

              then

               A7: (f . c) <= (( max (f,(g * h))) . c) by FUZZY_1: 5;

              (f . c) >= 0 by Th1;

              then ((f . c) * (h . c)) <= ((f . c) * 1) by A6, XREAL_1: 64;

              hence thesis by A2, A5, A7, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

          suppose

           A8: ( max ((f . c),(g . c))) = (g . c);

          (( max ((f . c),(g . c))) * ( max ((f . c),(h . c)))) <= (( max (f,(g * h))) . c)

          proof

            per cases by XXREAL_0: 16;

              suppose

               A9: ( max ((f . c),(h . c))) = (f . c);

              

               A10: 1 >= (g . c) by Th1;

              (f . c) <= ( max ((f . c),((g * h) . c))) by XXREAL_0: 25;

              then

               A11: (f . c) <= (( max (f,(g * h))) . c) by FUZZY_1: 5;

              (f . c) >= 0 by Th1;

              then ((f . c) * (g . c)) <= ((f . c) * 1) by A10, XREAL_1: 64;

              hence thesis by A8, A9, A11, XXREAL_0: 2;

            end;

              suppose

               A12: ( max ((f . c),(h . c))) = (h . c);

              (( max (f,(g * h))) . c) = ( max ((f . c),((g * h) . c))) by FUZZY_1: 5;

              then (( max (f,(g * h))) . c) >= ((g * h) . c) by XXREAL_0: 25;

              hence thesis by A8, A12, Def2;

            end;

          end;

          hence thesis;

        end;

      end;

      ((( max (f,g)) * ( max (f,h))) . c) = ((( max (f,g)) . c) * (( max (f,h)) . c)) by Def2

      .= (( max ((f . c),(g . c))) * (( max (f,h)) . c)) by FUZZY_1: 5

      .= (( max ((f . c),(g . c))) * ( max ((f . c),(h . c)))) by FUZZY_1: 5;

      hence thesis by A1;

    end;

    theorem :: FUZZY_2:48

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

    proof

      let c;

      

       A1: (( min ((f . c),(g . c))) * ( min ((f . c),(h . c)))) <= (( min (f,(g * h))) . c)

      proof

        now

          per cases by XXREAL_0: 15;

            suppose

             A2: ( min ((f . c),(g . c))) = (f . c);

            (( min ((f . c),(g . c))) * ( min ((f . c),(h . c)))) <= (( min (f,(g * h))) . c)

            proof

              per cases by XXREAL_0: 15;

                suppose

                 A3: ( min ((f . c),(h . c))) = (f . c);

                

                 A4: 0 <= (g . c) by Th1;

                (f . c) <= (h . c) by A3, XXREAL_0:def 9;

                then

                 A5: ((g . c) * (f . c)) <= ((h . c) * (g . c)) by A4, XREAL_1: 64;

                

                 A6: 0 <= (f . c) by Th1;

                (f * f) c= f by Th28;

                then

                 A7: ((f * f) . c) <= (f . c);

                (f . c) <= (g . c) by A2, XXREAL_0:def 9;

                then ((f . c) * (f . c)) <= ((g . c) * (f . c)) by A6, XREAL_1: 64;

                then ((f . c) * (f . c)) <= ((g . c) * (h . c)) by A5, XXREAL_0: 2;

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

                then ( min (((f . c) * (f . c)),((f . c) * (f . c)))) <= ( min ((f . c),((g . c) * (h . c)))) by Def2;

                then ((f . c) * (f . c)) <= ( min ((f . c),((g * h) . c))) by Def2;

                hence thesis by A2, A3, FUZZY_1: 5;

              end;

                suppose

                 A8: ( min ((f . c),(h . c))) = (h . c);

                

                 A9: 1 >= (h . c) by Th1;

                

                 A10: (h . c) >= 0 by Th1;

                (f . c) <= (g . c) by A2, XXREAL_0:def 9;

                then

                 A11: ((f . c) * (h . c)) <= ((g . c) * (h . c)) by A10, XREAL_1: 64;

                (f . c) >= 0 by Th1;

                then ((f . c) * (h . c)) <= ((f . c) * 1) by A9, XREAL_1: 64;

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

                then ((f . c) * (h . c)) <= ( min ((f . c),((g * h) . c))) by Def2;

                hence thesis by A2, A8, FUZZY_1: 5;

              end;

            end;

            hence thesis;

          end;

            suppose

             A12: ( min ((f . c),(g . c))) = (g . c);

            (( min ((f . c),(g . c))) * ( min ((f . c),(h . c)))) <= (( min (f,(g * h))) . c)

            proof

              per cases by XXREAL_0: 15;

                suppose

                 A13: ( min ((f . c),(h . c))) = (f . c);

                

                 A14: (g . c) >= 0 by Th1;

                (f . c) <= (h . c) by A13, XXREAL_0:def 9;

                then

                 A15: ((f . c) * (g . c)) <= ((h . c) * (g . c)) by A14, XREAL_1: 64;

                

                 A16: 1 >= (g . c) by Th1;

                (f . c) >= 0 by Th1;

                then ((g . c) * (f . c)) <= ((f . c) * 1) by A16, XREAL_1: 64;

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

                then ((f . c) * (g . c)) <= ( min ((f . c),((g * h) . c))) by Def2;

                hence thesis by A12, A13, FUZZY_1: 5;

              end;

                suppose

                 A17: ( min ((f . c),(h . c))) = (h . c);

                

                 A18: (g . c) <= (f . c) by A12, XXREAL_0:def 9;

                (f . c) >= 0 by Th1;

                then

                 A19: ((g . c) * (f . c)) <= ((f . c) * (f . c)) by A18, XREAL_1: 64;

                (f * f) c= f by Th28;

                then ((f * f) . c) <= (f . c);

                then

                 A20: ((f . c) * (f . c)) <= (f . c) by Def2;

                

                 A21: (h . c) <= (f . c) by A17, XXREAL_0:def 9;

                (g . c) >= 0 by Th1;

                then ((h . c) * (g . c)) <= ((f . c) * (g . c)) by A21, XREAL_1: 64;

                then ((h . c) * (g . c)) <= ((f . c) * (f . c)) by A19, XXREAL_0: 2;

                then ((h . c) * (g . c)) <= (f . c) by A20, XXREAL_0: 2;

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

                then ((g . c) * (h . c)) <= ( min ((f . c),((g * h) . c))) by Def2;

                hence thesis by A12, A17, FUZZY_1: 5;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      ((( min (f,g)) * ( min (f,h))) . c) = ((( min (f,g)) . c) * (( min (f,h)) . c)) by Def2

      .= (( min ((f . c),(g . c))) * (( min (f,h)) . c)) by FUZZY_1: 5

      .= (( min ((f . c),(g . c))) * ( min ((f . c),(h . c)))) by FUZZY_1: 5;

      hence thesis by A1;

    end;

    theorem :: FUZZY_2:49

    

     Th49: for c be Element of C, f,g be Membership_Func of C holds ((f ++ g) . c) = (1 - ((1 - (f . c)) * (1 - (g . c))))

    proof

      let c;

      let g,h be Membership_Func of C;

      ((g ++ h) . c) = (( 1_minus (( 1_minus g) * ( 1_minus h))) . c) by Th36

      .= (1 - ((( 1_minus g) * ( 1_minus h)) . c)) by FUZZY_1:def 5

      .= (1 - ((( 1_minus g) . c) * (( 1_minus h) . c))) by Def2

      .= (1 - ((1 - (g . c)) * (( 1_minus h) . c))) by FUZZY_1:def 5;

      hence thesis by FUZZY_1:def 5;

    end;

    theorem :: FUZZY_2:50

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

    proof

      let c;

      

       A1: ((( max (f,g)) ++ ( max (f,h))) . c) = (((( max (f,g)) . c) + (( max (f,h)) . c)) - ((( max (f,g)) . c) * (( max (f,h)) . c))) by Def3

      .= ((( max ((f . c),(g . c))) + (( max (f,h)) . c)) - ((( max (f,g)) . c) * (( max (f,h)) . c))) by FUZZY_1: 5

      .= ((( max ((f . c),(g . c))) + ( max ((f . c),(h . c)))) - ((( max (f,g)) . c) * (( max (f,h)) . c))) by FUZZY_1: 5

      .= ((( max ((f . c),(g . c))) + ( max ((f . c),(h . c)))) - (( max ((f . c),(g . c))) * (( max (f,h)) . c))) by FUZZY_1: 5

      .= ((( max ((f . c),(g . c))) + ( max ((f . c),(h . c)))) - (( max ((f . c),(g . c))) * ( max ((f . c),(h . c))))) by FUZZY_1: 5;

      

       A2: ( max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) <= ((( max ((f . c),(g . c))) + ( max ((f . c),(h . c)))) - (( max ((f . c),(g . c))) * ( max ((f . c),(h . c)))))

      proof

        per cases by XXREAL_0: 16;

          suppose

           A3: ( max ((f . c),(g . c))) = (f . c) & ( max ((f . c),(h . c))) = (f . c);

          (( 1_minus g) . c) >= 0 by Th1;

          then

           A4: (1 - (g . c)) >= 0 by FUZZY_1:def 5;

          (h . c) <= (f . c) by A3, XXREAL_0:def 10;

          then (1 - (h . c)) >= (1 - (f . c)) by XREAL_1: 10;

          then

           A5: ((1 - (g . c)) * (1 - (f . c))) <= ((1 - (g . c)) * (1 - (h . c))) by A4, XREAL_1: 64;

          (( 1_minus f) . c) >= 0 by Th1;

          then

           A6: (1 - (f . c)) >= 0 by FUZZY_1:def 5;

          f c= (f ++ f) by Th28;

          then ((f ++ f) . c) >= (f . c);

          then

           A7: (((f . c) + (f . c)) - ((f . c) * (f . c))) >= (f . c) by Def3;

          (g . c) <= (f . c) by A3, XXREAL_0:def 10;

          then (1 - (g . c)) >= (1 - (f . c)) by XREAL_1: 10;

          then ((1 - (f . c)) * (1 - (f . c))) <= ((1 - (g . c)) * (1 - (f . c))) by A6, XREAL_1: 64;

          then ((1 - (f . c)) * (1 - (f . c))) <= ((1 - (g . c)) * (1 - (h . c))) by A5, XXREAL_0: 2;

          then (1 - ((1 - (f . c)) * (1 - (f . c)))) >= (1 - ((1 - (g . c)) * (1 - (h . c)))) by XREAL_1: 10;

          hence thesis by A3, A7, XXREAL_0: 28;

        end;

          suppose

           A8: ( max ((f . c),(g . c))) = (f . c) & ( max ((f . c),(h . c))) = (h . c);

          (( 1_minus f) . c) >= 0 by Th1;

          then

           A9: (1 - (f . c)) >= 0 by FUZZY_1:def 5;

          (h . c) >= 0 by Th1;

          then ( 0 * (h . c)) <= ((h . c) * (1 - (f . c))) by A9, XREAL_1: 64;

          then

           A10: ( 0 + (f . c)) <= (((h . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

          (( 1_minus h) . c) >= 0 by Th1;

          then

           A11: (1 - (h . c)) >= 0 by FUZZY_1:def 5;

          (g . c) <= (f . c) by A8, XXREAL_0:def 10;

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

          then ((1 - (f . c)) * (1 - (h . c))) <= ((1 - (g . c)) * (1 - (h . c))) by A11, XREAL_1: 64;

          then (1 - ((1 - (f . c)) * (1 - (h . c)))) >= (1 - ((1 - (g . c)) * (1 - (h . c)))) by XREAL_1: 10;

          hence thesis by A8, A10, XXREAL_0: 28;

        end;

          suppose

           A12: ( max ((f . c),(g . c))) = (g . c) & ( max ((f . c),(h . c))) = (f . c);

          (( 1_minus f) . c) >= 0 by Th1;

          then

           A13: (1 - (f . c)) >= 0 by FUZZY_1:def 5;

          (g . c) >= 0 by Th1;

          then ( 0 * (g . c)) <= ((g . c) * (1 - (f . c))) by A13, XREAL_1: 64;

          then

           A14: ( 0 + (f . c)) <= (((g . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

          (( 1_minus g) . c) >= 0 by Th1;

          then

           A15: (1 - (g . c)) >= 0 by FUZZY_1:def 5;

          (h . c) <= (f . c) by A12, XXREAL_0:def 10;

          then (1 - (f . c)) <= (1 - (h . c)) by XREAL_1: 10;

          then ((1 - (f . c)) * (1 - (g . c))) <= ((1 - (h . c)) * (1 - (g . c))) by A15, XREAL_1: 64;

          then (1 - ((1 - (f . c)) * (1 - (g . c)))) >= (1 - ((1 - (h . c)) * (1 - (g . c)))) by XREAL_1: 10;

          hence thesis by A12, A14, XXREAL_0: 28;

        end;

          suppose

           A16: ( max ((f . c),(g . c))) = (g . c) & ( max ((f . c),(h . c))) = (h . c);

          (( 1_minus g) . c) >= 0 by Th1;

          then

           A17: (1 - (g . c)) >= 0 by FUZZY_1:def 5;

          (h . c) >= (f . c) by A16, XXREAL_0:def 10;

          then (1 - (h . c)) <= (1 - (f . c)) by XREAL_1: 10;

          then

           A18: ((1 - (g . c)) * (1 - (f . c))) >= ((1 - (g . c)) * (1 - (h . c))) by A17, XREAL_1: 64;

          (( 1_minus f) . c) >= 0 by Th1;

          then

           A19: (1 - (f . c)) >= 0 by FUZZY_1:def 5;

          (g . c) >= (f . c) by A16, XXREAL_0:def 10;

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

          then ((1 - (f . c)) * (1 - (f . c))) >= ((1 - (g . c)) * (1 - (f . c))) by A19, XREAL_1: 64;

          then ((1 - (f . c)) * (1 - (f . c))) >= ((1 - (g . c)) * (1 - (h . c))) by A18, XXREAL_0: 2;

          then (1 - ((1 - (f . c)) * (1 - (f . c)))) <= (1 - ((1 - (g . c)) * (1 - (h . c)))) by XREAL_1: 10;

          then

           A20: ((f ++ f) . c) <= (1 - ((1 - (g . c)) * (1 - (h . c)))) by Th49;

          f c= (f ++ f) by Th28;

          then ((f ++ f) . c) >= (f . c);

          then (f . c) <= (1 - ((1 - (g . c)) * (1 - (h . c)))) by A20, XXREAL_0: 2;

          hence thesis by A16, XXREAL_0: 28;

        end;

      end;

      (( max (f,(g ++ h))) . c) = ( max ((f . c),((g ++ h) . c))) by FUZZY_1: 5

      .= ( max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) by Th49;

      hence thesis by A1, A2;

    end;

    theorem :: FUZZY_2:51

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

    proof

      let c;

      

       A1: ((( min (f,g)) ++ ( min (f,h))) . c) = (((( min (f,g)) . c) + (( min (f,h)) . c)) - ((( min (f,g)) . c) * (( min (f,h)) . c))) by Def3

      .= ((( min ((f . c),(g . c))) + (( min (f,h)) . c)) - ((( min (f,g)) . c) * (( min (f,h)) . c))) by FUZZY_1: 5

      .= ((( min ((f . c),(g . c))) + ( min ((f . c),(h . c)))) - ((( min (f,g)) . c) * (( min (f,h)) . c))) by FUZZY_1: 5

      .= ((( min ((f . c),(g . c))) + ( min ((f . c),(h . c)))) - (( min ((f . c),(g . c))) * (( min (f,h)) . c))) by FUZZY_1: 5

      .= ((( min ((f . c),(g . c))) + ( min ((f . c),(h . c)))) - (( min ((f . c),(g . c))) * ( min ((f . c),(h . c))))) by FUZZY_1: 5;

      

       A2: ( min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) <= ((( min ((f . c),(g . c))) + ( min ((f . c),(h . c)))) - (( min ((f . c),(g . c))) * ( min ((f . c),(h . c)))))

      proof

        now

          per cases by XXREAL_0: 15;

            suppose

             A3: ( min ((f . c),(g . c))) = (f . c) & ( min ((f . c),(h . c))) = (f . c);

            f c= (f ++ f) by Th28;

            then

             A4: ((f ++ f) . c) >= (f . c);

            ( min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) <= (f . c) by XXREAL_0: 17;

            then ( min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) <= ((f ++ f) . c) by A4, XXREAL_0: 2;

            hence thesis by A3, Def3;

          end;

            suppose

             A5: ( min ((f . c),(g . c))) = (f . c) & ( min ((f . c),(h . c))) = (h . c);

            (( 1_minus f) . c) >= 0 by Th1;

            then

             A6: (1 - (f . c)) >= 0 by FUZZY_1:def 5;

            (h . c) >= 0 by Th1;

            then ( 0 * (h . c)) <= ((h . c) * (1 - (f . c))) by A6, XREAL_1: 64;

            then

             A7: ( 0 + (f . c)) <= (((h . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

            ( min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) <= (f . c) by XXREAL_0: 17;

            hence thesis by A5, A7, XXREAL_0: 2;

          end;

            suppose

             A8: ( min ((f . c),(g . c))) = (g . c) & ( min ((f . c),(h . c))) = (f . c);

            (( 1_minus f) . c) >= 0 by Th1;

            then

             A9: (1 - (f . c)) >= 0 by FUZZY_1:def 5;

            (g . c) >= 0 by Th1;

            then ( 0 * (g . c)) <= ((g . c) * (1 - (f . c))) by A9, XREAL_1: 64;

            then

             A10: ( 0 + (f . c)) <= (((g . c) * (1 - (f . c))) + (f . c)) by XREAL_1: 6;

            ( min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) <= (f . c) by XXREAL_0: 17;

            hence thesis by A8, A10, XXREAL_0: 2;

          end;

            suppose ( min ((f . c),(g . c))) = (g . c) & ( min ((f . c),(h . c))) = (h . c);

            hence thesis by XXREAL_0: 17;

          end;

        end;

        hence thesis;

      end;

      (( min (f,(g ++ h))) . c) = ( min ((f . c),((g ++ h) . c))) by FUZZY_1: 5

      .= ( min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))) by Th49;

      hence thesis by A1, A2;

    end;

    begin

    reserve C1,C2 for non empty set;

    registration

      let C be non empty set;

      cluster -> quasi_total for Membership_Func of C;

      coherence ;

    end

    definition

      let C1,C2 be non empty set;

      mode RMembership_Func of C1,C2 is Membership_Func of [:C1, C2:];

    end

    reserve f,g for RMembership_Func of C1, C2;

    definition

      let C1,C2 be non empty set;

      :: FUZZY_2:def4

      func Zmf (C1,C2) -> RMembership_Func of C1, C2 equals ( chi ( {} , [:C1, C2:]));

      correctness by FUZZY_1: 12;

      :: FUZZY_2:def5

      func Umf (C1,C2) -> RMembership_Func of C1, C2 equals ( chi ( [:C1, C2:], [:C1, C2:]));

      correctness by FUZZY_1: 1;

    end

    theorem :: FUZZY_2:52

    for x be Element of [:C1, C2:], h be RMembership_Func of C1, C2 holds (( Zmf (C1,C2)) . x) <= (h . x) & (h . x) <= (( Umf (C1,C2)) . x)

    proof

      

       A1: ( Umf (C1,C2)) = ( UMF [:C1, C2:]);

      ( Zmf (C1,C2)) = ( EMF [:C1, C2:]);

      hence thesis by A1, FUZZY_1: 16;

    end;

    theorem :: FUZZY_2:53

    ( max (f,( Umf (C1,C2)))) = ( Umf (C1,C2)) & ( min (f,( Umf (C1,C2)))) = f & ( max (f,( Zmf (C1,C2)))) = f & ( min (f,( Zmf (C1,C2)))) = ( Zmf (C1,C2))

    proof

      

       A1: ( Umf (C1,C2)) = ( UMF [:C1, C2:]);

      ( Zmf (C1,C2)) = ( EMF [:C1, C2:]);

      hence thesis by A1, FUZZY_1: 18;

    end;

    theorem :: FUZZY_2:54

    ( 1_minus ( Zmf (C1,C2))) = ( Umf (C1,C2)) & ( 1_minus ( Umf (C1,C2))) = ( Zmf (C1,C2))

    proof

      

       A1: ( Umf (C1,C2)) = ( UMF [:C1, C2:]);

      ( Zmf (C1,C2)) = ( EMF [:C1, C2:]);

      hence thesis by A1, FUZZY_1: 40;

    end;

    theorem :: FUZZY_2:55

    (f \ g) = ( Zmf (C1,C2)) implies f c= g

    proof

      ( Zmf (C1,C2)) = ( EMF [:C1, C2:]);

      hence thesis by Th26;

    end;

    theorem :: FUZZY_2:56

    ( min (f,g)) = ( Zmf (C1,C2)) implies (f \ g) = f

    proof

      ( Zmf (C1,C2)) = ( EMF [:C1, C2:]);

      hence thesis by Th27;

    end;