fuzzy_4.miz



    begin

    reserve c,c1,c2,x,y,z,z1,z2 for set;

    reserve C1,C2,C3 for non empty set;

    registration

      let C1 be non empty set;

      let F be Membership_Func of C1;

      cluster ( rng F) -> non empty;

      coherence

      proof

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

        then

        consider y be Element of C1 such that

         A1: y in ( dom F) by SUBSET_1: 4;

        (F . y) in ( rng F) by A1, FUNCT_1:def 3;

        hence thesis;

      end;

    end

    reconsider jj = 1 as Real;

    theorem :: FUZZY_4:1

    

     Th1: for F be Membership_Func of C1 holds ( rng F) is real-bounded & (for x st x in ( dom F) holds (F . x) <= ( upper_bound ( rng F))) & for x st x in ( dom F) holds (F . x) >= ( lower_bound ( rng F))

    proof

      let F be Membership_Func of C1;

      

       A1: [. 0 , jj.] is non empty closed_interval Subset of REAL by MEASURE5: 14;

      

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

      then

       A3: ( rng F) is real-bounded by A1, XXREAL_2: 45;

      

       A4: for x st x in ( dom F) holds (F . x) >= ( lower_bound ( rng F))

      proof

        let x;

        assume x in ( dom F);

        then

         A5: (F . x) in ( rng F) by FUNCT_1:def 3;

        ( rng F) is bounded_below by A3, XXREAL_2:def 11;

        hence thesis by A5, SEQ_4:def 2;

      end;

      for x st x in ( dom F) holds (F . x) <= ( upper_bound ( rng F))

      proof

        let x;

        assume x in ( dom F);

        then

         A6: (F . x) in ( rng F) by FUNCT_1:def 3;

        ( rng F) is bounded_above by A3, XXREAL_2:def 11;

        hence thesis by A6, SEQ_4:def 1;

      end;

      hence thesis by A2, A1, A4, XXREAL_2: 45;

    end;

    theorem :: FUZZY_4:2

    for F,G be Membership_Func of C1 holds (for x st x in C1 holds (F . x) <= (G . x)) implies ( upper_bound ( rng F)) <= ( upper_bound ( rng G))

    proof

      let F,G be Membership_Func of C1;

      ( rng F) is real-bounded by Th1;

      then

       A1: ( rng F) is bounded_above by XXREAL_2:def 11;

      assume

       A2: for c st c in C1 holds (F . c) <= (G . c);

      

       A3: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) <= (G . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A4: r in ( rng F) and

         A5: (( upper_bound ( rng F)) - s) < r by A1, SEQ_4:def 1;

        consider y be object such that

         A6: y in ( dom F) and

         A7: r = (F . y) by A4, FUNCT_1:def 3;

        r <= (G . y) by A2, A6, A7;

        hence thesis by A5, A6, XXREAL_0: 2;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng G))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A8: y in ( dom F) and

         A9: (( upper_bound ( rng F)) - s) <= (G . y) by A3;

        y in C1 by A8;

        then y in ( dom G) by FUNCT_2:def 1;

        then (G . y) <= ( upper_bound ( rng G)) by Th1;

        hence thesis by A9, XXREAL_0: 2;

      end;

      hence thesis by XREAL_1: 57;

    end;

    theorem :: FUZZY_4:3

    

     Th3: for f be RMembership_Func of C1, C2, c be set holds 0 <= (f . c) & (f . c) <= 1

    proof

      let f be RMembership_Func of C1, C2;

      let c be set;

      per cases ;

        suppose c in [:C1, C2:];

        then

        reconsider c as Element of [:C1, C2:];

        

         A1: (f . c) <= (( Umf (C1,C2)) . c) by FUZZY_2: 52;

        (( Zmf (C1,C2)) . c) <= (f . c) by FUZZY_2: 52;

        hence thesis by A1, FUNCT_3:def 3;

      end;

        suppose

         A2: not c in [:C1, C2:];

        ( dom f) = [:C1, C2:] by FUNCT_2:def 1;

        hence thesis by A2, FUNCT_1:def 2;

      end;

    end;

    theorem :: FUZZY_4:4

    for f be RMembership_Func of C1, C2, x, y holds 0 <= (f . (x,y)) & (f . (x,y)) <= 1 by Th3;

    begin

    notation

      let C1,C2 be non empty set;

      let h be RMembership_Func of C2, C1;

      synonym converse h for ~ h;

    end

    definition

      let C1,C2 be non empty set;

      let h be RMembership_Func of C2, C1;

      :: original: converse

      redefine

      :: FUZZY_4:def1

      func converse h -> RMembership_Func of C1, C2 means

      : Def1: for x,y be object st [x, y] in [:C1, C2:] holds (it . (x,y)) = (h . (y,x));

      coherence

      proof

        set IT = ( converse h);

        

         A1: ( dom h) = [:C2, C1:] by FUNCT_2:def 1;

        then

         A2: ( dom IT) = [:C1, C2:] by FUNCT_4: 46;

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

        then

         A3: ( rng IT) c= [. 0 , 1.] by A1, FUNCT_4: 47;

        then ( rng IT) c= REAL by MEMBERED: 3;

        then

        reconsider IT as PartFunc of [:C1, C2:], REAL by A2, RELSET_1: 4;

        IT is Membership_Func of [:C1, C2:] by A2, A3, FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis;

      end;

      compatibility

      proof

        let IT be RMembership_Func of C1, C2;

        

         A4: ( dom h) = [:C2, C1:] by FUNCT_2:def 1;

        thus IT = ( ~ h) implies for x,y be object st [x, y] in [:C1, C2:] holds (IT . (x,y)) = (h . (y,x))

        proof

          assume

           A5: IT = ( ~ h);

          let x,y be object;

          assume [x, y] in [:C1, C2:];

          then [y, x] in ( dom h) by A4, ZFMISC_1: 88;

          hence thesis by A5, FUNCT_4:def 2;

        end;

        

         A6: ( dom IT) = [:C1, C2:] by FUNCT_2:def 1;

        

         A7: for x be object holds x in ( dom IT) iff ex y,z be object st x = [z, y] & [y, z] in ( dom h)

        proof

          let x be object;

          thus x in ( dom IT) implies ex y,z be object st x = [z, y] & [y, z] in ( dom h)

          proof

            assume x in ( dom IT);

            then

            consider z,y be object such that

             A8: z in C1 and

             A9: y in C2 and

             A10: x = [z, y] by ZFMISC_1:def 2;

            reconsider y, z as set by TARSKI: 1;

            take y, z;

            thus thesis by A4, A8, A9, A10, ZFMISC_1:def 2;

          end;

          thus thesis by A6, ZFMISC_1: 88;

        end;

        assume for x,y be object st [x, y] in [:C1, C2:] holds (IT . (x,y)) = (h . (y,x));

        then for y,z be object st [y, z] in ( dom h) holds (IT . (z,y)) = (h . (y,z)) by ZFMISC_1: 88;

        hence thesis by A7, FUNCT_4:def 2;

      end;

    end

    theorem :: FUZZY_4:5

    for f be RMembership_Func of C1, C2 holds ( converse ( converse f)) = f

    proof

      let f be RMembership_Func of C1, C2;

      

       A1: ( dom f) = [:C1, C2:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C1, C2:] st c in [:C1, C2:] holds (( converse ( converse f)) . c) = (f . c)

      proof

        let c be Element of [:C1, C2:];

        assume c in [:C1, C2:];

        consider x,y be object such that

         A3: x in C1 and

         A4: y in C2 and

         A5: c = [x, y] by ZFMISC_1:def 2;

        

         A6: [y, x] in [:C2, C1:] by A3, A4, ZFMISC_1: 87;

        (( converse ( converse f)) . (x,y)) = (( converse f) . (y,x)) by A5, Def1

        .= (f . (x,y)) by A6, Def1;

        hence thesis by A5;

      end;

      ( dom ( converse ( converse f))) = [:C1, C2:] by FUNCT_2:def 1;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:6

    

     Th6: for f be RMembership_Func of C1, C2 holds ( 1_minus ( converse f)) = ( converse ( 1_minus f))

    proof

      let f be RMembership_Func of C1, C2;

      

       A1: [:C2, C1:] = ( dom ( converse ( 1_minus f))) by FUNCT_2:def 1;

      

       A2: for c be Element of [:C2, C1:] st c in [:C2, C1:] holds (( 1_minus ( converse f)) . c) = (( converse ( 1_minus f)) . c)

      proof

        let c be Element of [:C2, C1:];

        assume c in [:C2, C1:];

        consider y,x be object such that

         A3: y in C2 and

         A4: x in C1 and

         A5: c = [y, x] by ZFMISC_1:def 2;

        reconsider y, x as set by TARSKI: 1;

        

         A6: [x, y] in [:C1, C2:] by A3, A4, ZFMISC_1: 87;

        (( 1_minus ( converse f)) . (y,x)) = (1 - (( converse f) . (y,x))) by A5, FUZZY_1:def 5

        .= (1 - (f . (x,y))) by A5, Def1

        .= (( 1_minus f) . (x,y)) by A6, FUZZY_1:def 5

        .= (( converse ( 1_minus f)) . (y,x)) by A5, Def1;

        hence thesis by A5;

      end;

      ( dom ( 1_minus ( converse f))) = [:C2, C1:] by FUNCT_2:def 1;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:7

    

     Th7: for f,g be RMembership_Func of C1, C2 holds ( converse ( max (f,g))) = ( max (( converse f),( converse g)))

    proof

      let f,g be RMembership_Func of C1, C2;

      

       A1: ( dom ( max (( converse f),( converse g)))) = [:C2, C1:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C2, C1:] st c in [:C2, C1:] holds (( converse ( max (f,g))) . c) = (( max (( converse f),( converse g))) . c)

      proof

        let c be Element of [:C2, C1:];

        assume c in [:C2, C1:];

        consider y,x be object such that

         A3: y in C2 and

         A4: x in C1 and

         A5: c = [y, x] by ZFMISC_1:def 2;

        reconsider y, x as set by TARSKI: 1;

        

         A6: [x, y] in [:C1, C2:] by A3, A4, ZFMISC_1: 87;

        (( converse ( max (f,g))) . (y,x)) = (( max (f,g)) . (x,y)) by A5, Def1

        .= ( max ((f . (x,y)),(g . (x,y)))) by A6, FUZZY_1:def 4

        .= ( max ((( converse f) . (y,x)),(g . (x,y)))) by A5, Def1

        .= ( max ((( converse f) . (y,x)),(( converse g) . (y,x)))) by A5, Def1

        .= (( max (( converse f),( converse g))) . (y,x)) by A5, FUZZY_1:def 4;

        hence thesis by A5;

      end;

      ( dom ( converse ( max (f,g)))) = [:C2, C1:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:8

    

     Th8: for f,g be RMembership_Func of C1, C2 holds ( converse ( min (f,g))) = ( min (( converse f),( converse g)))

    proof

      let f,g be RMembership_Func of C1, C2;

      

       A1: ( dom ( min (( converse f),( converse g)))) = [:C2, C1:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C2, C1:] st c in [:C2, C1:] holds (( converse ( min (f,g))) . c) = (( min (( converse f),( converse g))) . c)

      proof

        let c be Element of [:C2, C1:];

        assume c in [:C2, C1:];

        consider y,x be object such that

         A3: y in C2 and

         A4: x in C1 and

         A5: c = [y, x] by ZFMISC_1:def 2;

        reconsider y, x as set by TARSKI: 1;

        

         A6: [x, y] in [:C1, C2:] by A3, A4, ZFMISC_1: 87;

        (( converse ( min (f,g))) . (y,x)) = (( min (f,g)) . (x,y)) by A5, Def1

        .= ( min ((f . (x,y)),(g . (x,y)))) by A6, FUZZY_1:def 3

        .= ( min ((( converse f) . (y,x)),(g . (x,y)))) by A5, Def1

        .= ( min ((( converse f) . (y,x)),(( converse g) . (y,x)))) by A5, Def1;

        hence thesis by A5, FUZZY_1:def 3;

      end;

      ( dom ( converse ( min (f,g)))) = [:C2, C1:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:9

    

     Th9: for f,g be RMembership_Func of C1, C2, x, y st x in C1 & y in C2 holds (f . [x, y]) <= (g . [x, y]) implies (( converse f) . [y, x]) <= (( converse g) . [y, x])

    proof

      let f,g be RMembership_Func of C1, C2, x, y;

      assume that

       A1: x in C1 and

       A2: y in C2 and

       A3: (f . [x, y]) <= (g . [x, y]);

      

       A4: [y, x] in [:C2, C1:] by A1, A2, ZFMISC_1: 87;

      then

       A5: (g . (x,y)) = (( converse g) . (y,x)) by Def1;

      (f . (x,y)) = (( converse f) . (y,x)) by A4, Def1;

      hence thesis by A3, A5;

    end;

    theorem :: FUZZY_4:10

    for f,g be RMembership_Func of C1, C2 holds f c= g implies ( converse f) c= ( converse g)

    proof

      let f,g be RMembership_Func of C1, C2;

      assume

       A1: f c= g;

      let c be Element of [:C2, C1:];

      ex y,x be object st y in C2 & x in C1 & c = [y, x] by ZFMISC_1:def 2;

      then

      consider x,y be set such that

       A2: x in C1 and

       A3: y in C2 and

       A4: c = [y, x];

       [x, y] in [:C1, C2:] by A2, A3, ZFMISC_1: 87;

      then (f . [x, y]) <= (g . [x, y]) by A1;

      hence thesis by A2, A3, A4, Th9;

    end;

    theorem :: FUZZY_4:11

    for f,g be RMembership_Func of C1, C2 holds ( converse (f \ g)) = (( converse f) \ ( converse g))

    proof

      let f,g be RMembership_Func of C1, C2;

      ( converse (f \ g)) = ( min (( converse f),( converse ( 1_minus g)))) by Th8

      .= ( min (( converse f),( 1_minus ( converse g)))) by Th6;

      hence thesis;

    end;

    theorem :: FUZZY_4:12

    for f,g be RMembership_Func of C1, C2 holds ( converse (f \+\ g)) = (( converse f) \+\ ( converse g))

    proof

      let f,g be RMembership_Func of C1, C2;

      ( converse (f \+\ g)) = ( max (( converse ( min (f,( 1_minus g)))),( converse ( min (( 1_minus f),g))))) by Th7

      .= ( max (( min (( converse f),( converse ( 1_minus g)))),( converse ( min (( 1_minus f),g))))) by Th8

      .= ( max (( min (( converse f),( converse ( 1_minus g)))),( min (( converse ( 1_minus f)),( converse g))))) by Th8

      .= ( max (( min (( converse f),( 1_minus ( converse g)))),( min (( converse ( 1_minus f)),( converse g))))) by Th6

      .= ( max (( min (( converse f),( 1_minus ( converse g)))),( min (( 1_minus ( converse f)),( converse g))))) by Th6;

      hence thesis;

    end;

    begin

    definition

      let C1,C2,C3 be non empty set;

      let h be RMembership_Func of C1, C2;

      let g be RMembership_Func of C2, C3;

      let x,z be object;

      assume that

       A1: x in C1 and

       A2: z in C3;

      :: FUZZY_4:def2

      func min (h,g,x,z) -> Membership_Func of C2 means

      : Def2: for y be Element of C2 holds (it . y) = ( min ((h . [x, y]),(g . [y, z])));

      existence

      proof

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

        

         A3: for y,c1,c2 be object st y in C2 & P[y, c1] & P[y, c2] holds c1 = c2;

        

         A4: for y,c be object st y in C2 & P[y, c] holds c in REAL by XREAL_0:def 1;

        consider IT be PartFunc of C2, REAL such that

         A5: (for y be object holds y in ( dom IT) iff y in C2 & ex c be object st P[y, c]) & for y be object st y in ( dom IT) holds P[y, (IT . y)] from PARTFUN1:sch 2( A4, A3);

        

         A6: ( dom IT) = C2 & ( rng IT) c= [. 0 , 1.]

        proof

          C2 c= ( dom IT)

          proof

            let y be object;

            ( min ((h . [x, y]),(g . [y, z]))) is set by TARSKI: 1;

            hence thesis by A5;

          end;

          hence ( dom IT) = C2 by XBOOLE_0:def 10;

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

          let c be object;

          

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

          assume c in ( rng IT);

          then

          consider y be Element of C2 such that

           A9: y in ( dom IT) and

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

          

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

           [x, y] in [:C1, C2:] by A1, ZFMISC_1: 87;

          then [x, y] in ( dom h) by FUNCT_2:def 1;

          then

           A12: (h . [x, y]) in ( rng h) by FUNCT_1:def 3;

           [y, z] in [:C2, C3:] by A2, ZFMISC_1: 87;

          then [y, z] in ( dom g) by FUNCT_2:def 1;

          then

           A13: (g . [y, z]) in ( rng g) by FUNCT_1:def 3;

          

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

          then

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

          

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

          then (h . [x, y]) <= 1 by A8, A12, INTEGRA2: 1;

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

          then

           A17: (IT . y) <= 1 by A5, A9;

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

          then

           A18: 0 <= (g . [y, z]) by A15, A13, INTEGRA2: 1;

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

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

          then 0 <= (IT . y) by A5, A9;

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

        end;

        then

         A19: IT is Membership_Func of C2 by FUNCT_2:def 1, RELAT_1:def 19;

        for y be Element of C2 holds (IT . y) = ( min ((h . [x, y]),(g . [y, z]))) by A5, A6;

        hence thesis by A19;

      end;

      uniqueness

      proof

        let F,G be Membership_Func of C2;

        assume that

         A20: for y be Element of C2 holds (F . y) = ( min ((h . [x, y]),(g . [y, z]))) and

         A21: for y be Element of C2 holds (G . y) = ( min ((h . [x, y]),(g . [y, z])));

        

         A22: for y be Element of C2 st y in C2 holds (F . y) = (G . y)

        proof

          let y be Element of C2;

          (F . y) = ( min ((h . [x, y]),(g . [y, z]))) by A20;

          hence thesis by A21;

        end;

        

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

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

        hence thesis by A23, A22, PARTFUN1: 5;

      end;

    end

    definition

      let C1,C2,C3 be non empty set;

      let h be RMembership_Func of C1, C2;

      let g be RMembership_Func of C2, C3;

      :: FUZZY_4:def3

      func h (#) g -> RMembership_Func of C1, C3 means

      : Def3: for x,z be object st [x, z] in [:C1, C3:] holds (it . (x,z)) = ( upper_bound ( rng ( min (h,g,x,z))));

      existence

      proof

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

        

         A1: for x,z,c1,c2 be object st x in C1 & z in C3 & P[x, z, c1] & P[x, z, c2] holds c1 = c2;

        

         A2: for x,z,c be object st x in C1 & z in C3 & P[x, z, c] holds c in REAL by XREAL_0:def 1;

        consider IT be PartFunc of [:C1, C3:], REAL such that

         A3: (for x,z be object holds [x, z] in ( dom IT) iff x in C1 & z in C3 & ex c be object st P[x, z, c]) & for x,z be object st [x, z] in ( dom IT) holds P[x, z, (IT . (x,z))] from BINOP_1:sch 5( A2, A1);

         [:C1, C3:] c= ( dom IT)

        proof

          let x,z be object;

          

           A5: ( upper_bound ( rng ( min (h,g,x,z)))) is set by TARSKI: 1;

          assume

           A6: [x, z] in [:C1, C3:];

          then

           A7: z in C3 by ZFMISC_1: 87;

          x in C1 by A6, ZFMISC_1: 87;

          hence thesis by A3, A5, A7;

        end;

        then

         A8: ( dom IT) = [:C1, C3:];

        ( rng IT) c= [. 0 , 1.]

        proof

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

          let c be object;

          assume c in ( rng IT);

          then

          consider a be Element of [:C1, C3:] such that a in ( dom IT) and

           A10: c = (IT . a) by PARTFUN1: 3;

          

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

          then

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

          

           A13: 0 <= ( upper_bound ( rng ( min (h,g,x,z)))) & ( upper_bound ( rng ( min (h,g,x,z)))) <= 1

          proof

            

             A14: ( rng ( min (h,g,x,z))) c= A by RELAT_1:def 19;

            A is bounded_below by INTEGRA1: 3;

            then

             A15: ( lower_bound A) <= ( lower_bound ( rng ( min (h,g,x,z)))) by A14, SEQ_4: 47;

            A is bounded_above by INTEGRA1: 3;

            then

             A16: ( upper_bound ( rng ( min (h,g,x,z)))) <= ( upper_bound A) by A14, SEQ_4: 48;

            ( lower_bound ( rng ( min (h,g,x,z)))) <= ( upper_bound ( rng ( min (h,g,x,z)))) by Th1, SEQ_4: 11;

            hence thesis by A11, A16, A15, INTEGRA1: 5;

          end;

          consider x,z be object such that x in C1 and z in C3 and

           A17: a = [x, z] by ZFMISC_1:def 2;

          reconsider z, x as set by TARSKI: 1;

          

           A18: (IT . (x,z)) = ( upper_bound ( rng ( min (h,g,x,z)))) by A3, A8, A17;

          then

           A19: (IT . a) <= 1 by A13, A17;

          

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

           0 <= (IT . a) by A13, A17, A18;

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

        end;

        then IT is RMembership_Func of C1, C3 by A8, FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis by A3, A8;

      end;

      uniqueness

      proof

        let F,G be RMembership_Func of C1, C3;

        assume that

         A21: for x,z be object st [x, z] in [:C1, C3:] holds (F . (x,z)) = ( upper_bound ( rng ( min (h,g,x,z)))) and

         A22: for x,z be object st [x, z] in [:C1, C3:] holds (G . (x,z)) = ( upper_bound ( rng ( min (h,g,x,z))));

        

         A23: for c be Element of [:C1, C3:] st c in [:C1, C3:] holds (F . c) = (G . c)

        proof

          let c be Element of [:C1, C3:];

          consider x,z be object such that x in C1 and z in C3 and

           A24: c = [x, z] by ZFMISC_1:def 2;

          reconsider z, x as set by TARSKI: 1;

          

           A25: (G . (x,z)) = ( upper_bound ( rng ( min (h,g,x,z)))) by A22, A24;

          (F . (x,z)) = ( upper_bound ( rng ( min (h,g,x,z)))) by A21, A24;

          hence thesis by A24, A25;

        end;

        

         A26: ( dom G) = [:C1, C3:] by FUNCT_2:def 1;

        ( dom F) = [:C1, C3:] by FUNCT_2:def 1;

        hence thesis by A26, A23, PARTFUN1: 5;

      end;

    end

    

     Lm1: for f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (f,( max (g,h)),x,z)))) = ( max (( upper_bound ( rng ( min (f,g,x,z)))),( upper_bound ( rng ( min (f,h,x,z))))))

    proof

      let f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      

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

      proof

        let y be Element of C2;

        assume y in C2;

        

         A4: [y, z] in [:C2, C3:] by A2, ZFMISC_1: 87;

        (( max (( min (f,g,x,z)),( min (f,h,x,z)))) . y) = ( max ((( min (f,g,x,z)) . y),(( min (f,h,x,z)) . y))) by FUZZY_1:def 4

        .= ( max ((( min (f,g,x,z)) . y),( min ((f . [x, y]),(h . [y, z]))))) by A1, A2, Def2

        .= ( max (( min ((f . [x, y]),(g . [y, z]))),( min ((f . [x, y]),(h . [y, z]))))) by A1, A2, Def2

        .= ( min ((f . [x, y]),( max ((g . [y, z]),(h . [y, z]))))) by XXREAL_0: 38

        .= ( min ((f . [x, y]),(( max (g,h)) . [y, z]))) by A4, FUZZY_1:def 4

        .= (( min (f,( max (g,h)),x,z)) . y) by A1, A2, Def2;

        hence thesis;

      end;

      set F = ( min (f,g,x,z)), G = ( min (f,h,x,z));

      

       A5: ( dom ( min (f,( max (g,h)),x,z))) = C2 by FUNCT_2:def 1;

      ( rng ( max (F,G))) is real-bounded by Th1;

      then

       A6: ( rng ( max (F,G))) is bounded_above by XXREAL_2:def 11;

      

       A7: for s be Real st 0 < s holds ex y st y in ( dom ( max (F,G))) & (( upper_bound ( rng ( max (F,G)))) - s) < (( max (F,G)) . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A8: r in ( rng ( max (F,G))) and

         A9: (( upper_bound ( rng ( max (F,G)))) - s) < r by A6, SEQ_4:def 1;

        ex y be object st y in ( dom ( max (F,G))) & r = (( max (F,G)) . y) by A8, FUNCT_1:def 3;

        hence thesis by A9;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng ( max (F,G)))) - s) < ( max (( upper_bound ( rng F)),( upper_bound ( rng G))))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A10: y in ( dom ( max (F,G))) and

         A11: (( upper_bound ( rng ( max (F,G)))) - s) < (( max (F,G)) . y) by A7;

        

         A12: (( max (F,G)) . y) = ( max ((F . y),(G . y))) by A10, FUZZY_1:def 4;

        

         A13: for y st y in C2 holds (F . y) <= ( upper_bound ( rng F)) & (G . y) <= ( upper_bound ( rng G))

        proof

          let y;

          assume

           A14: y in C2;

          then y in ( dom G) by FUNCT_2:def 1;

          then

           A15: (G . y) in ( rng G) by FUNCT_1:def 3;

          ( rng G) is real-bounded by Th1;

          then

           A16: ( rng G) is bounded_above by XXREAL_2:def 11;

          ( rng F) is real-bounded by Th1;

          then

           A17: ( rng F) is bounded_above by XXREAL_2:def 11;

          y in ( dom F) by A14, FUNCT_2:def 1;

          then (F . y) in ( rng F) by FUNCT_1:def 3;

          hence thesis by A15, A17, A16, SEQ_4:def 1;

        end;

        then

         A18: (G . y) <= ( upper_bound ( rng G)) by A10;

        (F . y) <= ( upper_bound ( rng F)) by A10, A13;

        then (( max (F,G)) . y) <= ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) by A12, A18, XXREAL_0: 26;

        hence thesis by A11, XXREAL_0: 2;

      end;

      then for s be Real st 0 < s holds (( upper_bound ( rng ( max (F,G)))) - s) <= ( max (( upper_bound ( rng F)),( upper_bound ( rng G))));

      then

       A19: ( upper_bound ( rng ( max (F,G)))) <= ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) by XREAL_1: 57;

      

       A20: for y st y in C2 holds (( max (F,G)) . y) <= ( upper_bound ( rng ( max (F,G))))

      proof

        let y;

        assume y in C2;

        then y in ( dom ( max (F,G))) by FUNCT_2:def 1;

        then

         A21: (( max (F,G)) . y) in ( rng ( max (F,G))) by FUNCT_1:def 3;

        ( rng ( max (F,G))) is real-bounded by Th1;

        then ( rng ( max (F,G))) is bounded_above by XXREAL_2:def 11;

        hence thesis by A21, SEQ_4:def 1;

      end;

      ( rng G) is real-bounded by Th1;

      then

       A22: ( rng G) is bounded_above by XXREAL_2:def 11;

      

       A23: for s be Real st 0 < s holds ex y st y in ( dom G) & (( upper_bound ( rng G)) - s) < (G . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A24: r in ( rng G) and

         A25: (( upper_bound ( rng G)) - s) < r by A22, SEQ_4:def 1;

        ex y be object st y in ( dom G) & r = (G . y) by A24, FUNCT_1:def 3;

        hence thesis by A25;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng G)) - s) <= ( upper_bound ( rng ( max (F,G))))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A26: y in ( dom G) and

         A27: (( upper_bound ( rng G)) - s) < (G . y) by A23;

        (G . y) <= ( max ((F . y),(G . y))) by XXREAL_0: 25;

        then (G . y) <= (( max (F,G)) . y) by A26, FUZZY_1:def 4;

        then

         A28: (( upper_bound ( rng G)) - s) < (( max (F,G)) . y) by A27, XXREAL_0: 2;

        (( max (F,G)) . y) <= ( upper_bound ( rng ( max (F,G)))) by A20, A26;

        hence thesis by A28, XXREAL_0: 2;

      end;

      then

       A29: ( upper_bound ( rng G)) <= ( upper_bound ( rng ( max (F,G)))) by XREAL_1: 57;

      ( rng F) is real-bounded by Th1;

      then

       A30: ( rng F) is bounded_above by XXREAL_2:def 11;

      

       A31: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) < (F . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A32: r in ( rng F) and

         A33: (( upper_bound ( rng F)) - s) < r by A30, SEQ_4:def 1;

        ex y be object st y in ( dom F) & r = (F . y) by A32, FUNCT_1:def 3;

        hence thesis by A33;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng ( max (F,G))))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A34: y in ( dom F) and

         A35: (( upper_bound ( rng F)) - s) < (F . y) by A31;

        (F . y) <= ( max ((F . y),(G . y))) by XXREAL_0: 25;

        then (F . y) <= (( max (F,G)) . y) by A34, FUZZY_1:def 4;

        then

         A36: (( upper_bound ( rng F)) - s) < (( max (F,G)) . y) by A35, XXREAL_0: 2;

        (( max (F,G)) . y) <= ( upper_bound ( rng ( max (F,G)))) by A20, A34;

        hence thesis by A36, XXREAL_0: 2;

      end;

      then ( upper_bound ( rng F)) <= ( upper_bound ( rng ( max (F,G)))) by XREAL_1: 57;

      then ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) <= ( upper_bound ( rng ( max (F,G)))) by A29, XXREAL_0: 28;

      then

       A37: ( upper_bound ( rng ( max (F,G)))) = ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) by A19, XXREAL_0: 1;

      ( dom ( max (( min (f,g,x,z)),( min (f,h,x,z))))) = C2 by FUNCT_2:def 1;

      hence thesis by A5, A3, A37, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:13

    for f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3 holds (f (#) ( max (g,h))) = ( max ((f (#) g),(f (#) h)))

    proof

      let f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3;

      

       A1: ( dom ( max ((f (#) g),(f (#) h)))) = [:C1, C3:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C1, C3:] st c in [:C1, C3:] holds ((f (#) ( max (g,h))) . c) = (( max ((f (#) g),(f (#) h))) . c)

      proof

        let c be Element of [:C1, C3:];

        consider x,z be object such that

         A3: x in C1 and

         A4: z in C3 and

         A5: c = [x, z] by ZFMISC_1:def 2;

        reconsider z, x as set by TARSKI: 1;

        ((f (#) ( max (g,h))) . c) = ((f (#) ( max (g,h))) . (x,z)) by A5

        .= ( upper_bound ( rng ( min (f,( max (g,h)),x,z)))) by A5, Def3

        .= ( max (( upper_bound ( rng ( min (f,g,x,z)))),( upper_bound ( rng ( min (f,h,x,z)))))) by A3, A4, Lm1

        .= ( max (((f (#) g) . (x,z)),( upper_bound ( rng ( min (f,h,x,z)))))) by A5, Def3

        .= ( max (((f (#) g) . (x,z)),((f (#) h) . (x,z)))) by A5, Def3

        .= (( max ((f (#) g),(f (#) h))) . c) by A5, FUZZY_1:def 4;

        hence thesis;

      end;

      ( dom (f (#) ( max (g,h)))) = [:C1, C3:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    

     Lm2: for f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (( max (f,g)),h,x,z)))) = ( max (( upper_bound ( rng ( min (f,h,x,z)))),( upper_bound ( rng ( min (g,h,x,z))))))

    proof

      let f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      

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

      proof

        let y be Element of C2;

        assume y in C2;

        

         A4: [x, y] in [:C1, C2:] by A1, ZFMISC_1: 87;

        (( min (( max (f,g)),h,x,z)) . y) = ( min ((( max (f,g)) . [x, y]),(h . [y, z]))) by A1, A2, Def2

        .= ( min (( max ((f . [x, y]),(g . [x, y]))),(h . [y, z]))) by A4, FUZZY_1:def 4

        .= ( max (( min ((f . [x, y]),(h . [y, z]))),( min ((g . [x, y]),(h . [y, z]))))) by XXREAL_0: 38

        .= ( max (( min ((f . [x, y]),(h . [y, z]))),(( min (g,h,x,z)) . y))) by A1, A2, Def2

        .= ( max ((( min (f,h,x,z)) . y),(( min (g,h,x,z)) . y))) by A1, A2, Def2;

        hence thesis by FUZZY_1:def 4;

      end;

      set F = ( min (f,h,x,z)), G = ( min (g,h,x,z));

      

       A5: ( dom ( max (( min (f,h,x,z)),( min (g,h,x,z))))) = C2 by FUNCT_2:def 1;

      ( rng ( max (F,G))) is real-bounded by Th1;

      then

       A6: ( rng ( max (F,G))) is bounded_above by XXREAL_2:def 11;

      

       A7: for y st y in ( dom ( max (F,G))) holds (( max (F,G)) . y) <= ( upper_bound ( rng ( max (F,G))))

      proof

        let y;

        assume y in ( dom ( max (F,G)));

        then (( max (F,G)) . y) in ( rng ( max (F,G))) by FUNCT_1:def 3;

        hence thesis by A6, SEQ_4:def 1;

      end;

      ( rng G) is real-bounded by Th1;

      then

       A8: ( rng G) is bounded_above by XXREAL_2:def 11;

      

       A9: for y st y in ( dom G) holds (G . y) <= ( upper_bound ( rng G))

      proof

        let y;

        assume y in ( dom G);

        then (G . y) in ( rng G) by FUNCT_1:def 3;

        hence thesis by A8, SEQ_4:def 1;

      end;

      

       A10: for s be Real st 0 < s holds ex y st y in ( dom G) & (( upper_bound ( rng G)) - s) <= (( max (F,G)) . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A11: r in ( rng G) and

         A12: (( upper_bound ( rng G)) - s) < r by A8, SEQ_4:def 1;

        consider y be object such that

         A13: y in ( dom G) and

         A14: r = (G . y) by A11, FUNCT_1:def 3;

        (G . y) <= ( max ((F . y),(G . y))) by XXREAL_0: 25;

        then r <= (( max (F,G)) . y) by A13, A14, FUZZY_1:def 4;

        hence thesis by A12, A13, XXREAL_0: 2;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng G)) - s) <= ( upper_bound ( rng ( max (F,G))))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A15: y in ( dom G) and

         A16: (( upper_bound ( rng G)) - s) <= (( max (F,G)) . y) by A10;

        y in C2 by A15;

        then y in ( dom ( max (F,G))) by FUNCT_2:def 1;

        then (( max (F,G)) . y) <= ( upper_bound ( rng ( max (F,G)))) by A7;

        hence thesis by A16, XXREAL_0: 2;

      end;

      then

       A17: ( upper_bound ( rng G)) <= ( upper_bound ( rng ( max (F,G)))) by XREAL_1: 57;

      ( rng F) is real-bounded by Th1;

      then

       A18: ( rng F) is bounded_above by XXREAL_2:def 11;

      

       A19: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) <= (( max (F,G)) . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A20: r in ( rng F) and

         A21: (( upper_bound ( rng F)) - s) < r by A18, SEQ_4:def 1;

        consider y be object such that

         A22: y in ( dom F) and

         A23: r = (F . y) by A20, FUNCT_1:def 3;

        (F . y) <= ( max ((F . y),(G . y))) by XXREAL_0: 25;

        then r <= (( max (F,G)) . y) by A22, A23, FUZZY_1:def 4;

        hence thesis by A21, A22, XXREAL_0: 2;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng ( max (F,G))))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A24: y in ( dom F) and

         A25: (( upper_bound ( rng F)) - s) <= (( max (F,G)) . y) by A19;

        y in C2 by A24;

        then y in ( dom ( max (F,G))) by FUNCT_2:def 1;

        then (( max (F,G)) . y) <= ( upper_bound ( rng ( max (F,G)))) by A7;

        hence thesis by A25, XXREAL_0: 2;

      end;

      then ( upper_bound ( rng F)) <= ( upper_bound ( rng ( max (F,G)))) by XREAL_1: 57;

      then

       A26: ( upper_bound ( rng ( max (F,G)))) >= ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) by A17, XXREAL_0: 28;

      

       A27: for y st y in ( dom F) holds (F . y) <= ( upper_bound ( rng F))

      proof

        let y;

        assume y in ( dom F);

        then (F . y) in ( rng F) by FUNCT_1:def 3;

        hence thesis by A18, SEQ_4:def 1;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng ( max (F,G)))) - s) <= ( max (( upper_bound ( rng F)),( upper_bound ( rng G))))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A28: r in ( rng ( max (F,G))) and

         A29: (( upper_bound ( rng ( max (F,G)))) - s) < r by A6, SEQ_4:def 1;

        consider y be object such that

         A30: y in ( dom ( max (F,G))) and

         A31: r = (( max (F,G)) . y) by A28, FUNCT_1:def 3;

        

         A32: y in C2 by A30;

        then y in ( dom G) by FUNCT_2:def 1;

        then

         A33: (G . y) <= ( upper_bound ( rng G)) by A9;

        y in ( dom F) by A32, FUNCT_2:def 1;

        then (F . y) <= ( upper_bound ( rng F)) by A27;

        then

         A34: ( max ((F . y),(G . y))) <= ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) by A33, XXREAL_0: 26;

        (( upper_bound ( rng ( max (F,G)))) - s) <= ( max ((F . y),(G . y))) by A29, A30, A31, FUZZY_1:def 4;

        hence thesis by A34, XXREAL_0: 2;

      end;

      then

       A35: ( upper_bound ( rng ( max (F,G)))) <= ( max (( upper_bound ( rng F)),( upper_bound ( rng G)))) by XREAL_1: 57;

      ( dom ( min (( max (f,g)),h,x,z))) = C2 by FUNCT_2:def 1;

      then ( min (( max (f,g)),h,x,z)) = ( max (( min (f,h,x,z)),( min (g,h,x,z)))) by A5, A3, PARTFUN1: 5;

      hence thesis by A35, A26, XXREAL_0: 1;

    end;

    theorem :: FUZZY_4:14

    for f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3 holds (( max (f,g)) (#) h) = ( max ((f (#) h),(g (#) h)))

    proof

      let f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3;

      

       A1: ( dom ( max ((f (#) h),(g (#) h)))) = [:C1, C3:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C1, C3:] st c in [:C1, C3:] holds ((( max (f,g)) (#) h) . c) = (( max ((f (#) h),(g (#) h))) . c)

      proof

        let c be Element of [:C1, C3:];

        consider x,z be object such that

         A3: x in C1 and

         A4: z in C3 and

         A5: c = [x, z] by ZFMISC_1:def 2;

        reconsider z, x as set by TARSKI: 1;

        ((( max (f,g)) (#) h) . c) = ((( max (f,g)) (#) h) . (x,z)) by A5

        .= ( upper_bound ( rng ( min (( max (f,g)),h,x,z)))) by A5, Def3

        .= ( max (( upper_bound ( rng ( min (f,h,x,z)))),( upper_bound ( rng ( min (g,h,x,z)))))) by A3, A4, Lm2

        .= ( max (((f (#) h) . (x,z)),( upper_bound ( rng ( min (g,h,x,z)))))) by A5, Def3

        .= ( max (((f (#) h) . (x,z)),((g (#) h) . (x,z)))) by A5, Def3

        .= (( max ((f (#) h),(g (#) h))) . c) by A5, FUZZY_1:def 4;

        hence thesis;

      end;

      ( dom (( max (f,g)) (#) h)) = [:C1, C3:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    

     Lm3: for f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (f,( min (g,h)),x,z)))) <= ( min (( upper_bound ( rng ( min (f,g,x,z)))),( upper_bound ( rng ( min (f,h,x,z))))))

    proof

      let f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      set F = ( min (f,( min (g,h)),x,z)), G = ( min (f,g,x,z)), H = ( min (f,h,x,z));

      ( rng F) is real-bounded by Th1;

      then

       A3: ( rng F) is bounded_above by XXREAL_2:def 11;

      

       A4: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) <= (G . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A5: r in ( rng F) and

         A6: (( upper_bound ( rng F)) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A7: y in ( dom F) and

         A8: r = (F . y) by A5, FUNCT_1:def 3;

        

         A9: [y, z] in [:C2, C3:] by A2, A7, ZFMISC_1: 87;

        (F . y) = ( min ((f . [x, y]),(( min (g,h)) . [y, z]))) by A1, A2, A7, Def2

        .= ( min ((f . [x, y]),( min ((g . [y, z]),(h . [y, z]))))) by A9, FUZZY_1:def 3

        .= ( min (( min ((f . [x, y]),(g . [y, z]))),(h . [y, z]))) by XXREAL_0: 33

        .= ( min ((G . y),(h . [y, z]))) by A1, A2, A7, Def2;

        then r <= (G . y) by A8, XXREAL_0: 17;

        hence thesis by A6, A7, XXREAL_0: 2;

      end;

      

       A10: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) <= (H . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A11: r in ( rng F) and

         A12: (( upper_bound ( rng F)) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A13: y in ( dom F) and

         A14: r = (F . y) by A11, FUNCT_1:def 3;

        

         A15: [y, z] in [:C2, C3:] by A2, A13, ZFMISC_1: 87;

        (F . y) = ( min ((f . [x, y]),(( min (g,h)) . [y, z]))) by A1, A2, A13, Def2

        .= ( min ((f . [x, y]),( min ((g . [y, z]),(h . [y, z]))))) by A15, FUZZY_1:def 3

        .= ( min (( min ((f . [x, y]),(h . [y, z]))),(g . [y, z]))) by XXREAL_0: 33

        .= ( min ((H . y),(g . [y, z]))) by A1, A2, A13, Def2;

        then r <= (H . y) by A14, XXREAL_0: 17;

        hence thesis by A12, A13, XXREAL_0: 2;

      end;

      ( rng H) is real-bounded by Th1;

      then

       A16: ( rng H) is bounded_above by XXREAL_2:def 11;

      

       A17: for y st y in ( dom H) holds (H . y) <= ( upper_bound ( rng H))

      proof

        let y;

        assume y in ( dom H);

        then (H . y) in ( rng H) by FUNCT_1:def 3;

        hence thesis by A16, SEQ_4:def 1;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng H))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A18: y in ( dom F) and

         A19: (( upper_bound ( rng F)) - s) <= (H . y) by A10;

        y in C2 by A18;

        then y in ( dom H) by FUNCT_2:def 1;

        then (H . y) <= ( upper_bound ( rng H)) by A17;

        hence thesis by A19, XXREAL_0: 2;

      end;

      then

       A20: ( upper_bound ( rng F)) <= ( upper_bound ( rng H)) by XREAL_1: 57;

      ( rng G) is real-bounded by Th1;

      then

       A21: ( rng G) is bounded_above by XXREAL_2:def 11;

      

       A22: for y st y in ( dom G) holds (G . y) <= ( upper_bound ( rng G))

      proof

        let y;

        assume y in ( dom G);

        then (G . y) in ( rng G) by FUNCT_1:def 3;

        hence thesis by A21, SEQ_4:def 1;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng G))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A23: y in ( dom F) and

         A24: (( upper_bound ( rng F)) - s) <= (G . y) by A4;

        y in C2 by A23;

        then y in ( dom G) by FUNCT_2:def 1;

        then (G . y) <= ( upper_bound ( rng G)) by A22;

        hence thesis by A24, XXREAL_0: 2;

      end;

      then ( upper_bound ( rng F)) <= ( upper_bound ( rng G)) by XREAL_1: 57;

      hence thesis by A20, XXREAL_0: 20;

    end;

    theorem :: FUZZY_4:15

    for f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3 holds (f (#) ( min (g,h))) c= ( min ((f (#) g),(f (#) h)))

    proof

      let f be RMembership_Func of C1, C2, g,h be RMembership_Func of C2, C3;

      let c be Element of [:C1, C3:];

      consider x,z be object such that

       A1: x in C1 and

       A2: z in C3 and

       A3: c = [x, z] by ZFMISC_1:def 2;

      reconsider z, x as set by TARSKI: 1;

      

       A4: ((f (#) ( min (g,h))) . (x,z)) = ( upper_bound ( rng ( min (f,( min (g,h)),x,z)))) by A3, Def3;

      (( min ((f (#) g),(f (#) h))) . (x,z)) = ( min (((f (#) g) . (x,z)),((f (#) h) . (x,z)))) by A3, FUZZY_1:def 3

      .= ( min (((f (#) g) . (x,z)),( upper_bound ( rng ( min (f,h,x,z)))))) by A3, Def3

      .= ( min (( upper_bound ( rng ( min (f,g,x,z)))),( upper_bound ( rng ( min (f,h,x,z)))))) by A3, Def3;

      hence thesis by A1, A2, A3, A4, Lm3;

    end;

    

     Lm4: for f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (( min (f,g)),h,x,z)))) <= ( min (( upper_bound ( rng ( min (f,h,x,z)))),( upper_bound ( rng ( min (g,h,x,z))))))

    proof

      let f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      set F = ( min (( min (f,g)),h,x,z)), G = ( min (f,h,x,z)), H = ( min (g,h,x,z));

      ( rng F) is real-bounded by Th1;

      then

       A3: ( rng F) is bounded_above by XXREAL_2:def 11;

      

       A4: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) <= (G . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A5: r in ( rng F) and

         A6: (( upper_bound ( rng F)) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A7: y in ( dom F) and

         A8: r = (F . y) by A5, FUNCT_1:def 3;

        

         A9: [x, y] in [:C1, C2:] by A1, A7, ZFMISC_1: 87;

        (F . y) = ( min ((( min (f,g)) . [x, y]),(h . [y, z]))) by A1, A2, A7, Def2

        .= ( min (( min ((f . [x, y]),(g . [x, y]))),(h . [y, z]))) by A9, FUZZY_1:def 3

        .= ( min (( min ((h . [y, z]),(f . [x, y]))),(g . [x, y]))) by XXREAL_0: 33

        .= ( min ((G . y),(g . [x, y]))) by A1, A2, A7, Def2;

        then r <= (G . y) by A8, XXREAL_0: 17;

        hence thesis by A6, A7, XXREAL_0: 2;

      end;

      

       A10: for s be Real st 0 < s holds ex y st y in ( dom F) & (( upper_bound ( rng F)) - s) <= (H . y)

      proof

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         A11: r in ( rng F) and

         A12: (( upper_bound ( rng F)) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A13: y in ( dom F) and

         A14: r = (F . y) by A11, FUNCT_1:def 3;

        

         A15: [x, y] in [:C1, C2:] by A1, A13, ZFMISC_1: 87;

        (F . y) = ( min ((( min (f,g)) . [x, y]),(h . [y, z]))) by A1, A2, A13, Def2

        .= ( min (( min ((f . [x, y]),(g . [x, y]))),(h . [y, z]))) by A15, FUZZY_1:def 3

        .= ( min ((f . [x, y]),( min ((h . [y, z]),(g . [x, y]))))) by XXREAL_0: 33

        .= ( min ((H . y),(f . [x, y]))) by A1, A2, A13, Def2;

        then r <= (H . y) by A14, XXREAL_0: 17;

        hence thesis by A12, A13, XXREAL_0: 2;

      end;

      ( rng H) is real-bounded by Th1;

      then

       A16: ( rng H) is bounded_above by XXREAL_2:def 11;

      

       A17: for y st y in ( dom H) holds (H . y) <= ( upper_bound ( rng H))

      proof

        let y;

        assume y in ( dom H);

        then (H . y) in ( rng H) by FUNCT_1:def 3;

        hence thesis by A16, SEQ_4:def 1;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng H))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A18: y in ( dom F) and

         A19: (( upper_bound ( rng F)) - s) <= (H . y) by A10;

        y in C2 by A18;

        then y in ( dom H) by FUNCT_2:def 1;

        then (H . y) <= ( upper_bound ( rng H)) by A17;

        hence thesis by A19, XXREAL_0: 2;

      end;

      then

       A20: ( upper_bound ( rng F)) <= ( upper_bound ( rng H)) by XREAL_1: 57;

      ( rng G) is real-bounded by Th1;

      then

       A21: ( rng G) is bounded_above by XXREAL_2:def 11;

      

       A22: for y st y in ( dom G) holds (G . y) <= ( upper_bound ( rng G))

      proof

        let y;

        assume y in ( dom G);

        then (G . y) in ( rng G) by FUNCT_1:def 3;

        hence thesis by A21, SEQ_4:def 1;

      end;

      for s be Real st 0 < s holds (( upper_bound ( rng F)) - s) <= ( upper_bound ( rng G))

      proof

        let s be Real;

        assume 0 < s;

        then

        consider y such that

         A23: y in ( dom F) and

         A24: (( upper_bound ( rng F)) - s) <= (G . y) by A4;

        y in C2 by A23;

        then y in ( dom G) by FUNCT_2:def 1;

        then (G . y) <= ( upper_bound ( rng G)) by A22;

        hence thesis by A24, XXREAL_0: 2;

      end;

      then ( upper_bound ( rng F)) <= ( upper_bound ( rng G)) by XREAL_1: 57;

      hence thesis by A20, XXREAL_0: 20;

    end;

    theorem :: FUZZY_4:16

    for f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3 holds (( min (f,g)) (#) h) c= ( min ((f (#) h),(g (#) h)))

    proof

      let f,g be RMembership_Func of C1, C2, h be RMembership_Func of C2, C3;

      let c be Element of [:C1, C3:];

      consider x,z be object such that

       A1: x in C1 and

       A2: z in C3 and

       A3: c = [x, z] by ZFMISC_1:def 2;

      reconsider z, x as set by TARSKI: 1;

      

       A4: ((( min (f,g)) (#) h) . (x,z)) = ( upper_bound ( rng ( min (( min (f,g)),h,x,z)))) by A3, Def3;

      (( min ((f (#) h),(g (#) h))) . (x,z)) = ( min (((f (#) h) . (x,z)),((g (#) h) . (x,z)))) by A3, FUZZY_1:def 3

      .= ( min (( upper_bound ( rng ( min (f,h,x,z)))),((g (#) h) . (x,z)))) by A3, Def3

      .= ( min (( upper_bound ( rng ( min (f,h,x,z)))),( upper_bound ( rng ( min (g,h,x,z)))))) by A3, Def3;

      hence thesis by A1, A2, A3, A4, Lm4;

    end;

    

     Lm5: for f be RMembership_Func of C1, C2, g be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) = ( upper_bound ( rng ( min (f,g,x,z))))

    proof

      let f be RMembership_Func of C1, C2, g be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      ( rng ( min (f,g,x,z))) is real-bounded by Th1;

      then

       A3: ( rng ( min (f,g,x,z))) is bounded_above by XXREAL_2:def 11;

      for s be Real st 0 < s holds (( upper_bound ( rng ( min (f,g,x,z)))) - s) <= ( upper_bound ( rng ( min (( converse g),( converse f),z,x))))

      proof

        let s be Real;

        assume s > 0 ;

        then

        consider r be Real such that

         A4: r in ( rng ( min (f,g,x,z))) and

         A5: (( upper_bound ( rng ( min (f,g,x,z)))) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A6: y in ( dom ( min (f,g,x,z))) and

         A7: r = (( min (f,g,x,z)) . y) by A4, FUNCT_1:def 3;

        reconsider y as set by TARSKI: 1;

        

         A8: [z, y] in [:C3, C2:] by A2, A6, ZFMISC_1: 87;

        y in C2 by A6;

        then y in ( dom ( min (( converse g),( converse f),z,x))) by FUNCT_2:def 1;

        then

         A9: (( min (( converse g),( converse f),z,x)) . y) <= ( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) by Th1;

        

         A10: [y, x] in [:C2, C1:] by A1, A6, ZFMISC_1: 87;

        r = ( min ((f . (x,y)),(g . (y,z)))) by A1, A2, A6, A7, Def2

        .= ( min ((( converse f) . (y,x)),(g . (y,z)))) by A10, Def1

        .= ( min ((( converse f) . (y,x)),(( converse g) . (z,y)))) by A8, Def1

        .= (( min (( converse g),( converse f),z,x)) . y) by A1, A2, A6, Def2;

        hence thesis by A5, A9, XXREAL_0: 2;

      end;

      then

       A11: ( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) >= ( upper_bound ( rng ( min (f,g,x,z)))) by XREAL_1: 57;

      ( rng ( min (( converse g),( converse f),z,x))) is real-bounded by Th1;

      then

       A12: ( rng ( min (( converse g),( converse f),z,x))) is bounded_above by XXREAL_2:def 11;

      for s be Real st 0 < s holds (( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) - s) <= ( upper_bound ( rng ( min (f,g,x,z))))

      proof

        let s be Real;

        assume s > 0 ;

        then

        consider r be Real such that

         A13: r in ( rng ( min (( converse g),( converse f),z,x))) and

         A14: (( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) - s) < r by A12, SEQ_4:def 1;

        consider y be object such that

         A15: y in ( dom ( min (( converse g),( converse f),z,x))) and

         A16: r = (( min (( converse g),( converse f),z,x)) . y) by A13, FUNCT_1:def 3;

        

         A17: [z, y] in [:C3, C2:] by A2, A15, ZFMISC_1: 87;

        y in C2 by A15;

        then y in ( dom ( min (f,g,x,z))) by FUNCT_2:def 1;

        then

         A18: (( min (f,g,x,z)) . y) <= ( upper_bound ( rng ( min (f,g,x,z)))) by Th1;

        

         A19: [y, x] in [:C2, C1:] by A1, A15, ZFMISC_1: 87;

        reconsider y as set by TARSKI: 1;

        r = ( min ((( converse g) . (z,y)),(( converse f) . (y,x)))) by A1, A2, A15, A16, Def2

        .= ( min ((g . (y,z)),(( converse f) . (y,x)))) by A17, Def1

        .= ( min ((g . (y,z)),(f . (x,y)))) by A19, Def1

        .= (( min (f,g,x,z)) . y) by A1, A2, A15, Def2;

        hence thesis by A14, A18, XXREAL_0: 2;

      end;

      then ( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) <= ( upper_bound ( rng ( min (f,g,x,z)))) by XREAL_1: 57;

      hence thesis by A11, XXREAL_0: 1;

    end;

    theorem :: FUZZY_4:17

    for f be RMembership_Func of C1, C2, g be RMembership_Func of C2, C3 holds ( converse (f (#) g)) = (( converse g) (#) ( converse f))

    proof

      let f be RMembership_Func of C1, C2, g be RMembership_Func of C2, C3;

      

       A1: ( dom (( converse g) (#) ( converse f))) = [:C3, C1:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C3, C1:] st c in [:C3, C1:] holds (( converse (f (#) g)) . c) = ((( converse g) (#) ( converse f)) . c)

      proof

        let c be Element of [:C3, C1:];

        assume c in [:C3, C1:];

        consider z,x be object such that

         A3: z in C3 and

         A4: x in C1 and

         A5: c = [z, x] by ZFMISC_1:def 2;

        

         A6: [x, z] in [:C1, C3:] by A3, A4, ZFMISC_1: 87;

        reconsider z, x as set by TARSKI: 1;

        

         A7: ((( converse g) (#) ( converse f)) . (z,x)) = ( upper_bound ( rng ( min (( converse g),( converse f),z,x)))) by A5, Def3;

        (( converse (f (#) g)) . (z,x)) = ((f (#) g) . (x,z)) by A5, Def1

        .= ( upper_bound ( rng ( min (f,g,x,z)))) by A6, Def3;

        hence thesis by A3, A4, A5, A7, Lm5;

      end;

      ( dom ( converse (f (#) g))) = [:C3, C1:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:18

    

     Th18: for f,g be RMembership_Func of C1, C2, h,k be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 & (for y be set st y in C2 holds (f . [x, y]) <= (g . [x, y]) & (h . [y, z]) <= (k . [y, z])) holds ((f (#) h) . [x, z]) <= ((g (#) k) . [x, z])

    proof

      let f,g be RMembership_Func of C1, C2, h,k be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3 and

       A3: for y be set st y in C2 holds (f . [x, y]) <= (g . [x, y]) & (h . [y, z]) <= (k . [y, z]);

      

       A4: [x, z] in [:C1, C3:] by A1, A2, ZFMISC_1: 87;

      then

       A5: ((g (#) k) . (x,z)) = ( upper_bound ( rng ( min (g,k,x,z)))) by Def3;

      ( rng ( min (f,h,x,z))) is real-bounded by Th1;

      then

       A6: ( rng ( min (f,h,x,z))) is bounded_above by XXREAL_2:def 11;

      

       A7: for s be Real st s > 0 holds (( upper_bound ( rng ( min (f,h,x,z)))) - s) <= ( upper_bound ( rng ( min (g,k,x,z))))

      proof

        let s be Real;

        assume s > 0 ;

        then

        consider r be Real such that

         A8: r in ( rng ( min (f,h,x,z))) and

         A9: (( upper_bound ( rng ( min (f,h,x,z)))) - s) < r by A6, SEQ_4:def 1;

        consider y be object such that

         A10: y in ( dom ( min (f,h,x,z))) and

         A11: r = (( min (f,h,x,z)) . y) by A8, FUNCT_1:def 3;

        

         A12: (h . [y, z]) <= (k . [y, z]) by A3, A10;

        (f . [x, y]) <= (g . [x, y]) by A3, A10;

        then ( min ((f . [x, y]),(h . [y, z]))) <= ( min ((g . [x, y]),(k . [y, z]))) by A12, XXREAL_0: 18;

        then

         A13: (( min (f,h,x,z)) . y) <= ( min ((g . [x, y]),(k . [y, z]))) by A1, A2, A10, Def2;

        y in C2 by A10;

        then

         A14: y in ( dom ( min (g,k,x,z))) by FUNCT_2:def 1;

        ( min ((g . [x, y]),(k . [y, z]))) = (( min (g,k,x,z)) . y) by A1, A2, A10, Def2;

        then ( min ((g . [x, y]),(k . [y, z]))) <= ( upper_bound ( rng ( min (g,k,x,z)))) by A14, Th1;

        then (( min (f,h,x,z)) . y) <= ( upper_bound ( rng ( min (g,k,x,z)))) by A13, XXREAL_0: 2;

        hence thesis by A9, A11, XXREAL_0: 2;

      end;

      ((f (#) h) . (x,z)) = ( upper_bound ( rng ( min (f,h,x,z)))) by A4, Def3;

      hence thesis by A5, A7, XREAL_1: 57;

    end;

    theorem :: FUZZY_4:19

    for f,g be RMembership_Func of C1, C2, h,k be RMembership_Func of C2, C3 st f c= g & h c= k holds (f (#) h) c= (g (#) k)

    proof

      let f,g be RMembership_Func of C1, C2, h,k be RMembership_Func of C2, C3;

      assume that

       A1: f c= g and

       A2: h c= k;

      let c be Element of [:C1, C3:];

      consider x,z be object such that

       A3: x in C1 and

       A4: z in C3 and

       A5: c = [x, z] by ZFMISC_1:def 2;

      for y be set st y in C2 holds (f . [x, y]) <= (g . [x, y]) & (h . [y, z]) <= (k . [y, z])

      proof

        let y be set;

        assume

         A6: y in C2;

        then

         A7: [y, z] in [:C2, C3:] by A4, ZFMISC_1: 87;

         [x, y] in [:C1, C2:] by A3, A6, ZFMISC_1: 87;

        hence thesis by A1, A2, A7;

      end;

      hence thesis by A3, A4, A5, Th18;

    end;

    begin

    

     Lm6: 1 in REAL & 0 in REAL by XREAL_0:def 1;

    definition

      let C1,C2 be non empty set;

      :: FUZZY_4:def4

      func Imf (C1,C2) -> RMembership_Func of C1, C2 means

      : Def4: for x,y be object st [x, y] in [:C1, C2:] holds (x = y implies (it . (x,y)) = 1) & (x <> y implies (it . (x,y)) = 0 );

      existence

      proof

        defpred P[ object, object, object] means ($1 = $2 implies $3 = 1) & ( not $1 = $2 implies $3 = 0 );

        

         A1: for x,y,z1,z2 be object st x in C1 & y in C2 & P[x, y, z1] & P[x, y, z2] holds z1 = z2;

        

         A2: for x,y,z be object st x in C1 & y in C2 & P[x, y, z] holds z in REAL by Lm6;

        consider IT be PartFunc of [:C1, C2:], REAL such that

         A3: (for x,y be object holds [x, y] in ( dom IT) iff x in C1 & y in C2 & ex z be object st P[x, y, z]) & for x,y be object st [x, y] in ( dom IT) holds P[x, y, (IT . (x,y))] from BINOP_1:sch 5( A2, A1);

         [:C1, C2:] c= ( dom IT)

        proof

          let x,y be object;

          

           A4: not x = y implies ex z st (x = y implies z = 1) & ( not x = y implies z = 0 );

          assume

           A5: [x, y] in [:C1, C2:];

          then

           A6: y in C2 by ZFMISC_1: 87;

          x in C1 by A5, ZFMISC_1: 87;

          hence thesis by A3, A6, A4;

        end;

        then

         A7: ( dom IT) = [:C1, C2:];

        ( rng IT) c= [. 0 , 1.]

        proof

          let c be object;

          assume c in ( rng IT);

          then

          consider z be Element of [:C1, C2:] such that

           A8: z in ( dom IT) and

           A9: c = (IT . z) by PARTFUN1: 3;

          consider x,y be object such that x in C1 and y in C2 and

           A10: z = [x, y] by ZFMISC_1:def 2;

          

           A11: 1 in [. 0 , 1.] & 0 in [. 0 , 1.]

          proof

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

            

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

            then

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

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

            hence thesis by A13, INTEGRA2: 1;

          end;

          then

           A14: x <> y implies (IT . (x,y)) in [. 0 , 1.] by A3, A8, A10;

          x = y implies (IT . (x,y)) in [. 0 , 1.] by A3, A8, A10, A11;

          hence thesis by A9, A10, A14;

        end;

        then IT is RMembership_Func of C1, C2 by A7, FUNCT_2:def 1, RELAT_1:def 19;

        hence thesis by A3, A7;

      end;

      uniqueness

      proof

        let F,G be RMembership_Func of C1, C2;

        assume that

         A15: for x,y be object st [x, y] in [:C1, C2:] holds (x = y implies (F . (x,y)) = 1) & (x <> y implies (F . (x,y)) = 0 ) and

         A16: for x,y be object st [x, y] in [:C1, C2:] holds (x = y implies (G . (x,y)) = 1) & (x <> y implies (G . (x,y)) = 0 );

        

         A17: for x,y be object st x in C1 & y in C2 holds (F . (x,y)) = (G . (x,y))

        proof

          let x,y be object;

          assume that

           A18: x in C1 and

           A19: y in C2;

          

           A20: [x, y] in [:C1, C2:] by A18, A19, ZFMISC_1: 87;

          then

           A21: not x = y implies (F . (x,y)) = 0 by A15;

          x = y implies (F . (x,y)) = 1 by A15, A20;

          hence thesis by A16, A20, A21;

        end;

        thus thesis by A17;

      end;

    end

    theorem :: FUZZY_4:20

    for c be Element of [:C1, C2:] holds (( Zmf (C1,C2)) . c) = 0 & (( Umf (C1,C2)) . c) = 1 by FUNCT_3:def 3;

    theorem :: FUZZY_4:21

    for x, y st [x, y] in [:C1, C2:] holds (( Zmf (C1,C2)) . [x, y]) = 0 & (( Umf (C1,C2)) . [x, y]) = 1 by FUNCT_3:def 3;

    

     Lm7: for f be RMembership_Func of C2, C3, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) = (( Zmf (C1,C3)) . [x, z])

    proof

      let f be RMembership_Func of C2, C3, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      ( rng ( min (( Zmf (C1,C2)),f,x,z))) is real-bounded by Th1;

      then

       A3: ( rng ( min (( Zmf (C1,C2)),f,x,z))) is bounded_above by XXREAL_2:def 11;

      for s be Real st 0 < s holds (( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) - s) <= (( Zmf (C1,C3)) . [x, z])

      proof

        let s be Real;

        assume s > 0 ;

        then

        consider r be Real such that

         A4: r in ( rng ( min (( Zmf (C1,C2)),f,x,z))) and

         A5: (( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A6: y in ( dom ( min (( Zmf (C1,C2)),f,x,z))) and

         A7: r = (( min (( Zmf (C1,C2)),f,x,z)) . y) by A4, FUNCT_1:def 3;

        

         A8: [x, y] in [:C1, C2:] by A1, A6, ZFMISC_1: 87;

        

         A9: [x, z] in [:C1, C3:] by A1, A2, ZFMISC_1: 87;

        

         A10: 0 <= (f . [y, z]) by Th3;

        r = ( min ((( Zmf (C1,C2)) . [x, y]),(f . [y, z]))) by A1, A2, A6, A7, Def2

        .= ( min ( 0 ,(f . [y, z]))) by A8, FUNCT_3:def 3

        .= 0 by A10, XXREAL_0:def 9

        .= (( Zmf (C1,C3)) . [x, z]) by A9, FUNCT_3:def 3;

        hence thesis by A5;

      end;

      then

       A11: ( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) <= (( Zmf (C1,C3)) . [x, z]) by XREAL_1: 57;

      ( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) >= (( Zmf (C1,C3)) . [x, z])

      proof

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

        

         A12: A is bounded_below by INTEGRA1: 3;

        ( rng ( min (( Zmf (C1,C2)),f,x,z))) c= [. 0 , 1.] by RELAT_1:def 19;

        then

         A13: ( lower_bound A) <= ( lower_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) by A12, SEQ_4: 47;

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

        then

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

        

         A15: ( lower_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) <= ( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) by Th1, SEQ_4: 11;

         [x, z] in [:C1, C3:] by A1, A2, ZFMISC_1: 87;

        hence thesis by A14, A13, A15, FUNCT_3:def 3;

      end;

      hence thesis by A11, XXREAL_0: 1;

    end;

    theorem :: FUZZY_4:22

    

     Th22: for f be RMembership_Func of C2, C3 holds (( Zmf (C1,C2)) (#) f) = ( Zmf (C1,C3))

    proof

      let f be RMembership_Func of C2, C3;

      

       A1: ( dom ( Zmf (C1,C3))) = [:C1, C3:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C1, C3:] st c in [:C1, C3:] holds ((( Zmf (C1,C2)) (#) f) . c) = (( Zmf (C1,C3)) . c)

      proof

        let c be Element of [:C1, C3:];

        consider x,z be object such that

         A3: x in C1 and

         A4: z in C3 and

         A5: c = [x, z] by ZFMISC_1:def 2;

        reconsider z, x as set by TARSKI: 1;

        ((( Zmf (C1,C2)) (#) f) . c) = ((( Zmf (C1,C2)) (#) f) . (x,z)) by A5

        .= ( upper_bound ( rng ( min (( Zmf (C1,C2)),f,x,z)))) by A5, Def3

        .= (( Zmf (C1,C3)) . c) by A3, A4, A5, Lm7;

        hence thesis;

      end;

      ( dom (( Zmf (C1,C2)) (#) f)) = [:C1, C3:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    

     Lm8: for f be RMembership_Func of C1, C2, x,z be set st x in C1 & z in C3 holds ( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) = (( Zmf (C1,C3)) . [x, z])

    proof

      let f be RMembership_Func of C1, C2, x,z be set;

      assume that

       A1: x in C1 and

       A2: z in C3;

      ( rng ( min (f,( Zmf (C2,C3)),x,z))) is real-bounded by Th1;

      then

       A3: ( rng ( min (f,( Zmf (C2,C3)),x,z))) is bounded_above by XXREAL_2:def 11;

      for s be Real st 0 < s holds (( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) - s) <= (( Zmf (C1,C3)) . [x, z])

      proof

        let s be Real;

        assume s > 0 ;

        then

        consider r be Real such that

         A4: r in ( rng ( min (f,( Zmf (C2,C3)),x,z))) and

         A5: (( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) - s) < r by A3, SEQ_4:def 1;

        consider y be object such that

         A6: y in ( dom ( min (f,( Zmf (C2,C3)),x,z))) and

         A7: r = (( min (f,( Zmf (C2,C3)),x,z)) . y) by A4, FUNCT_1:def 3;

        

         A8: [y, z] in [:C2, C3:] by A2, A6, ZFMISC_1: 87;

        

         A9: [x, z] in [:C1, C3:] by A1, A2, ZFMISC_1: 87;

        

         A10: 0 <= (f . [x, y]) by Th3;

        r = ( min ((f . [x, y]),(( Zmf (C2,C3)) . [y, z]))) by A1, A2, A6, A7, Def2

        .= ( min ((f . [x, y]), 0 )) by A8, FUNCT_3:def 3

        .= 0 by A10, XXREAL_0:def 9

        .= (( Zmf (C1,C3)) . [x, z]) by A9, FUNCT_3:def 3;

        hence thesis by A5;

      end;

      then

       A11: ( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) <= (( Zmf (C1,C3)) . [x, z]) by XREAL_1: 57;

      ( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) >= (( Zmf (C1,C3)) . [x, z])

      proof

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

        

         A12: A is bounded_below by INTEGRA1: 3;

        ( rng ( min (f,( Zmf (C2,C3)),x,z))) c= [. 0 , 1.] by RELAT_1:def 19;

        then

         A13: ( lower_bound A) <= ( lower_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) by A12, SEQ_4: 47;

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

        then

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

        

         A15: ( lower_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) <= ( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) by Th1, SEQ_4: 11;

         [x, z] in [:C1, C3:] by A1, A2, ZFMISC_1: 87;

        hence thesis by A14, A13, A15, FUNCT_3:def 3;

      end;

      hence thesis by A11, XXREAL_0: 1;

    end;

    theorem :: FUZZY_4:23

    

     Th23: for f be RMembership_Func of C1, C2 holds (f (#) ( Zmf (C2,C3))) = ( Zmf (C1,C3))

    proof

      let f be RMembership_Func of C1, C2;

      

       A1: ( dom ( Zmf (C1,C3))) = [:C1, C3:] by FUNCT_2:def 1;

      

       A2: for c be Element of [:C1, C3:] st c in [:C1, C3:] holds ((f (#) ( Zmf (C2,C3))) . c) = (( Zmf (C1,C3)) . c)

      proof

        let c be Element of [:C1, C3:];

        consider x,z be object such that

         A3: x in C1 and

         A4: z in C3 and

         A5: c = [x, z] by ZFMISC_1:def 2;

        reconsider z, x as set by TARSKI: 1;

        ((f (#) ( Zmf (C2,C3))) . c) = ((f (#) ( Zmf (C2,C3))) . (x,z)) by A5

        .= ( upper_bound ( rng ( min (f,( Zmf (C2,C3)),x,z)))) by A5, Def3

        .= (( Zmf (C1,C3)) . c) by A3, A4, A5, Lm8;

        hence thesis;

      end;

      ( dom (f (#) ( Zmf (C2,C3)))) = [:C1, C3:] by FUNCT_2:def 1;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: FUZZY_4:24

    for f be RMembership_Func of C1, C1 holds (f (#) ( Zmf (C1,C1))) = (( Zmf (C1,C1)) (#) f)

    proof

      let f be RMembership_Func of C1, C1;

      (f (#) ( Zmf (C1,C1))) = ( Zmf (C1,C1)) by Th23;

      hence thesis by Th22;

    end;

    begin

    theorem :: FUZZY_4:25

    for X,Y be non empty set holds for x be Element of X, y be Element of Y holds (x = y implies (( Imf (X,Y)) . (x,y)) = 1) & (x <> y implies (( Imf (X,Y)) . (x,y)) = 0 )

    proof

      let X,Y be non empty set;

      let x be Element of X, y be Element of Y;

       [x, y] in [:X, Y:] by ZFMISC_1: 87;

      hence thesis by Def4;

    end;

    theorem :: FUZZY_4:26

    for X,Y be non empty set holds for x be Element of X, y be Element of Y holds for f be RMembership_Func of X, Y holds (( converse f) . (y,x)) = (f . (x,y)) by Def1, ZFMISC_1: 87;