fuznum_1.miz



    begin

    theorem :: FUZNUM_1:1

    

     RealNon: for a,b be Real st a <= b holds ( REAL \ ].a, b.[) <> {}

    proof

      let a,b be Real;

      assume a <= b;

      consider c be Real such that

       A1: c < a by XREAL_1: 2;

      

       A2: not c in ].a, b.[ by A1, XXREAL_1: 4;

      c in REAL by XREAL_0:def 1;

      hence thesis by A2, XBOOLE_0:def 5;

    end;

    reserve a,b,c,x for Real;

    theorem :: FUZNUM_1:2

    

     Ah1: (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . a) = 0

    proof

      (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . a) = (((1 / (b - a)) * a) + ( - (a / (b - a)))) by FCONT_1:def 4

      .= (((1 / (b - a)) * a) + (( - a) / (b - a))) by XCMPLX_1: 187

      .= (((1 / (b - a)) * a) + ((a * ( - 1)) / (b - a)))

      .= ((a * (1 / (b - a))) + (a * (( - 1) / (b - a)))) by XCMPLX_1: 74

      .= (a * ((1 / (b - a)) + (( - 1) / (b - a))))

      .= (a * ((1 / (b - a)) + ( - (1 / (b - a))))) by XCMPLX_1: 187

      .= 0 ;

      hence thesis;

    end;

    theorem :: FUZNUM_1:3

    

     Ab1: (b - a) <> 0 implies (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . b) = 1

    proof

      assume

       A1: (b - a) <> 0 ;

      (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . b) = (((1 / (b - a)) * b) + ( - (a / (b - a)))) by FCONT_1:def 4

      .= ((b / (b - a)) + ( - (a / (b - a)))) by XCMPLX_1: 99

      .= ((b / (b - a)) + (( - a) / (b - a))) by XCMPLX_1: 187

      .= ((b + ( - a)) / (b - a)) by XCMPLX_1: 62

      .= ((1 / (b - a)) * (b + ( - a))) by XCMPLX_1: 99

      .= 1 by XCMPLX_1: 106, A1;

      hence thesis;

    end;

    theorem :: FUZNUM_1:4

    

     Cb1: (c - b) <> 0 implies (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . b) = 1

    proof

      assume

       A1: (c - b) <> 0 ;

      (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . b) = ((( - (1 / (c - b))) * b) + (c / (c - b))) by FCONT_1:def 4

      .= (((( - 1) / (c - b)) * b) + (c / (c - b))) by XCMPLX_1: 187

      .= (((( - 1) * b) / (c - b)) + (c / (c - b))) by XCMPLX_1: 74

      .= ((( - b) + c) / (c - b)) by XCMPLX_1: 62

      .= 1 by A1, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: FUZNUM_1:5

    

     Cb2: (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . c) = 0

    proof

      (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . c) = ((( - (1 / (c - b))) * c) + (c / (c - b))) by FCONT_1:def 4

      .= (((( - 1) / (c - b)) * c) + (c / (c - b))) by XCMPLX_1: 187

      .= (((( - 1) * c) / (c - b)) + (c / (c - b))) by XCMPLX_1: 74

      .= ((( - c) + c) / (c - b)) by XCMPLX_1: 62

      .= 0 ;

      hence thesis;

    end;

    theorem :: FUZNUM_1:6

    

     Hope3: (b - a) <> 0 & (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . x) = 1 implies x = b

    proof

      assume that

       A0: (b - a) <> 0 and

       A1: (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . x) = 1;

      x in REAL & b in REAL by XREAL_0:def 1;

      then

       A3: x in ( dom ( AffineMap ((1 / (b - a)),( - (a / (b - a)))))) & b in ( dom ( AffineMap ((1 / (b - a)),( - (a / (b - a)))))) by FUNCT_2:def 1;

      (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . b) = 1 by A0, Ab1;

      hence thesis by A1, FUNCT_1:def 4, A3, A0;

    end;

    theorem :: FUZNUM_1:7

    

     Hope4: (c - b) <> 0 & (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . x) = 1 implies x = b

    proof

      assume that

       A0: (c - b) <> 0 and

       A1: (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . x) = 1;

      x in REAL & b in REAL by XREAL_0:def 1;

      then

       A3: x in ( dom ( AffineMap (( - (1 / (c - b))),(c / (c - b))))) & b in ( dom ( AffineMap (( - (1 / (c - b))),(c / (c - b))))) by FUNCT_2:def 1;

      (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . b) = 1 by A0, Cb1;

      hence thesis by A1, FUNCT_1:def 4, A3, A0;

    end;

    theorem :: FUZNUM_1:8

    ( rng ( AffineMap ( 0 ,a))) = {a}

    proof

      set f = ( AffineMap ( 0 ,a));

      thus ( rng f) c= {a}

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A1: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        reconsider x as Real by A1;

        y = (( 0 * x) + a) by A1, FCONT_1:def 4

        .= a;

        hence thesis by TARSKI:def 1;

      end;

      let y be object;

      assume

       a0: y in {a};

       0 in REAL by XREAL_0:def 1;

      then

       A1: 0 in ( dom f) by FUNCT_2:def 1;

      y = (( 0 * 0 ) + a) by a0, TARSKI:def 1

      .= (f . 0 ) by FCONT_1:def 4;

      hence thesis by FUNCT_1:def 3, A1;

    end;

    theorem :: FUZNUM_1:9

    

     Andr1a: for C be non empty Subset of REAL holds ( rng (( AffineMap ( 0 ,a)) | C)) = {a}

    proof

      let C be non empty Subset of REAL ;

      set f = (( AffineMap ( 0 ,a)) | C);

      thus ( rng f) c= {a}

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A1: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        reconsider x as Real by A1;

        y = (( AffineMap ( 0 ,a)) . x) by A1, FUNCT_1: 49;

        

        then y = (( 0 * x) + a) by FCONT_1:def 4

        .= a;

        hence thesis by TARSKI:def 1;

      end;

      let y be object;

      assume

       a0: y in {a};

      reconsider o = the Element of C as Real;

      C c= REAL ;

      then C c= ( dom ( AffineMap ( 0 ,a))) by FUNCT_2:def 1;

      then

       a1: ( dom f) = C by RELAT_1: 62;

      y = (( 0 * o) + a) by a0, TARSKI:def 1

      .= (( AffineMap ( 0 ,a)) . o) by FCONT_1:def 4

      .= (f . o) by FUNCT_1: 49;

      hence thesis by FUNCT_1:def 3, a1;

    end;

    theorem :: FUZNUM_1:10

    

     Hope1: (b - a) > 0 implies ( rng (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) = [. 0 , 1.]

    proof

      set f = ( AffineMap ((1 / (b - a)),( - (a / (b - a)))));

      set g = (f | [.a, b.]);

      assume

       A0: (b - a) > 0 ;

      thus ( rng g) c= [. 0 , 1.]

      proof

        let y be object;

        assume

         Y0: y in ( rng g);

        then

        consider x be object such that

         A1: x in ( dom g) and

         A2: y = (g . x) by FUNCT_1:def 3;

        

         Y1: x in [.a, b.] by A1, RELAT_1: 57;

        reconsider xx = x as Real by A1;

        reconsider yy = y as Real by Y0;

        

         S4: y = (f . xx) by FUNCT_1: 47, A1, A2;

        

         A4: a <= xx by Y1, XXREAL_1: 1;

        

         S2: (f . a) = 0 by Ah1;

        

         S5: (f . a) <= (f . xx) by A4, FCONT_1: 53, A0;

        xx <= b by Y1, XXREAL_1: 1;

        then

         S6: (f . xx) <= (f . b) by A0, FCONT_1: 53;

        (f . b) = 1 by Ab1, A0;

        hence thesis by S4, S2, S5, S6;

      end;

      let y be object;

      assume

       V1: y in [. 0 , 1.];

      then

      reconsider yy = y as Real;

      set A = (1 / (b - a));

      set B = ( - (a / (b - a)));

      

       L2: (f qua Function " ) = ( AffineMap ((A " ),( - (B / A)))) by A0, FCONT_1: 56;

      

      then

       L3: ((f qua Function " ) . 0 ) = (((A " ) * 0 ) + ( - (B / A))) by FCONT_1:def 4

      .= ( - ((( - a) / (b - a)) / (1 / (b - a)))) by XCMPLX_1: 187

      .= ( - (( - a) / 1)) by XCMPLX_1: 55, A0

      .= a;

      set x = ((f qua Function " ) . yy);

      reconsider xx = x as Real by L2;

      

       X1: ( - (B / A)) = ( - ((( - a) / (b - a)) / (1 / (b - a)))) by XCMPLX_1: 187

      .= ( - (( - a) / 1)) by XCMPLX_1: 55, A0

      .= a;

      

       L4: ((f qua Function " ) . 1) = (((A " ) * 1) + ( - (B / A))) by FCONT_1:def 4, L2

      .= ((1 / A) + ( - (B / A))) by XCMPLX_1: 215

      .= ((b - a) + a) by XCMPLX_1: 52, X1

      .= b;

      

       J2: 0 <= yy & yy <= 1 by XXREAL_1: 1, V1;

      then

       J3: a <= xx by FCONT_1: 53, L2, A0, L3;

      xx <= b by FCONT_1: 53, L2, A0, J2, L4;

      then

       J4: x in [.a, b.] by J3;

      

       j5: ( dom f) = REAL by FUNCT_2:def 1;

      

       T1: x in ( dom g) by J4, j5, RELAT_1: 57;

      ( rng f) = REAL by FCONT_1: 55, A0;

      then

       S2: yy in ( rng f) by XREAL_0:def 1;

      (g . ((f qua Function " ) . yy)) = (f . ((f qua Function " ) . yy)) by FUNCT_1: 49, J4

      .= yy by A0, S2, FUNCT_1: 35;

      hence thesis by T1, FUNCT_1:def 3;

    end;

    theorem :: FUZNUM_1:11

    (c - b) > 0 implies ( rng (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | ].b, c.])) = [. 0 , 1.[

    proof

      set f = ( AffineMap (( - (1 / (c - b))),(c / (c - b))));

      set g = (f | ].b, c.]);

      assume

       A0: (c - b) > 0 ;

      thus ( rng g) c= [. 0 , 1.[

      proof

        let y be object;

        assume

         Y0: y in ( rng g);

        then

        consider x be object such that

         A1: x in ( dom g) and

         A2: y = (g . x) by FUNCT_1:def 3;

        

         Y1: x in ].b, c.] by A1, RELAT_1: 57;

        reconsider xx = x as Real by A1;

        reconsider yy = y as Real by Y0;

        

         S4: y = (f . xx) by FUNCT_1: 47, A1, A2;

        

         A4: b < xx by Y1, XXREAL_1: 2;

        

         S2: (f . b) = 1 by Cb1, A0;

        

         S5: (f . b) > (f . xx) by A4, FCONT_1: 52, A0;

        xx <= c by Y1, XXREAL_1: 2;

        then

         S6: (f . xx) >= (f . c) by A0, FCONT_1: 54;

        (f . c) = 0 by Cb2;

        hence thesis by S4, S2, S5, S6;

      end;

      let y be object;

      assume

       V1: y in [. 0 , 1.[;

      then

      reconsider yy = y as Real;

      set A = ( - (1 / (c - b)));

      set B = (c / (c - b));

      

       L2: (f qua Function " ) = ( AffineMap ((A " ),( - (B / A)))) by A0, FCONT_1: 56;

      

      then

       L3: ((f qua Function " ) . 0 ) = (((A " ) * 0 ) + ( - (B / A))) by FCONT_1:def 4

      .= ( - ((c / (c - b)) / (( - 1) / (c - b)))) by XCMPLX_1: 187

      .= ( - (c / ( - 1))) by XCMPLX_1: 55, A0

      .= c;

      

       X1: ( - (B / A)) = ( - ((c / (c - b)) / (( - 1) / (c - b)))) by XCMPLX_1: 187

      .= ( - (c / ( - 1))) by XCMPLX_1: 55, A0

      .= c;

      

       L4: ((f qua Function " ) . 1) = (((A " ) * 1) + ( - (B / A))) by FCONT_1:def 4, L2

      .= ((1 / A) + ( - (B / A))) by XCMPLX_1: 215

      .= ((1 / (( - 1) / (c - b))) + c) by XCMPLX_1: 187, X1

      .= (((c - b) / ( - 1)) + c) by XCMPLX_1: 57

      .= b;

      set x = ((f qua Function " ) . yy);

      reconsider xx = x as Real by L2;

      

       J2: 0 <= yy & yy < 1 by XXREAL_1: 3, V1;

      then

       J3: c >= xx by FCONT_1: 54, L2, A0, L3;

      xx > b by FCONT_1: 52, L2, A0, J2, L4;

      then

       J4: x in ].b, c.] by J3;

      

       j5: ( dom f) = REAL by FUNCT_2:def 1;

      

       T1: x in ( dom g) by J4, j5, RELAT_1: 57;

      ( rng f) = REAL by FCONT_1: 55, A0;

      then

       S2: yy in ( rng f) by XREAL_0:def 1;

      set ff = (f qua Function " );

      (g . (ff . yy)) = (f . (ff . yy)) by FUNCT_1: 49, J4

      .= yy by A0, S2, FUNCT_1: 35;

      hence thesis by T1, FUNCT_1:def 3;

    end;

    theorem :: FUZNUM_1:12

    

     Hope2a: (c - b) > 0 implies ( rng (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) = [. 0 , 1.]

    proof

      set f = ( AffineMap (( - (1 / (c - b))),(c / (c - b))));

      set g = (f | [.b, c.]);

      assume

       A0: (c - b) > 0 ;

      thus ( rng g) c= [. 0 , 1.]

      proof

        let y be object;

        assume

         Y0: y in ( rng g);

        then

        consider x be object such that

         A1: x in ( dom g) and

         A2: y = (g . x) by FUNCT_1:def 3;

        

         Y1: x in [.b, c.] by A1, RELAT_1: 57;

        reconsider xx = x as Real by A1;

        reconsider yy = y as Real by Y0;

        

         S4: y = (f . xx) by FUNCT_1: 47, A1, A2;

        

         A4: b <= xx by Y1, XXREAL_1: 1;

        

         S2: (f . b) = 1 by Cb1, A0;

        

         S5: (f . b) >= (f . xx) by A4, FCONT_1: 54, A0;

        xx <= c by Y1, XXREAL_1: 1;

        then

         S6: (f . xx) >= (f . c) by A0, FCONT_1: 54;

        (f . c) = 0 by Cb2;

        hence thesis by S4, S2, S5, S6;

      end;

      let y be object;

      assume

       V1: y in [. 0 , 1.];

      then

      reconsider yy = y as Real;

      set A = ( - (1 / (c - b)));

      set B = (c / (c - b));

      

       L2: (f qua Function " ) = ( AffineMap ((A " ),( - (B / A)))) by FCONT_1: 56, A0;

      

      then

       L3: ((f qua Function " ) . 0 ) = (((A " ) * 0 ) + ( - (B / A))) by FCONT_1:def 4

      .= ( - ((c / (c - b)) / (( - 1) / (c - b)))) by XCMPLX_1: 187

      .= ( - (c / ( - 1))) by XCMPLX_1: 55, A0

      .= c;

      

       X1: ( - (B / A)) = ( - ((c / (c - b)) / (( - 1) / (c - b)))) by XCMPLX_1: 187

      .= ( - (c / ( - 1))) by XCMPLX_1: 55, A0

      .= c;

      

       L4: ((f qua Function " ) . 1) = (((A " ) * 1) + ( - (B / A))) by FCONT_1:def 4, L2

      .= ((1 / A) + ( - (B / A))) by XCMPLX_1: 215

      .= ((1 / (( - 1) / (c - b))) + c) by XCMPLX_1: 187, X1

      .= (((c - b) / ( - 1)) + c) by XCMPLX_1: 57

      .= b;

      set x = ((f qua Function " ) . yy);

      reconsider xx = x as Real by L2;

      

       J2: 0 <= yy & yy <= 1 by XXREAL_1: 1, V1;

      then

       J3: c >= xx by FCONT_1: 54, L2, A0, L3;

      xx >= b by FCONT_1: 54, L2, A0, J2, L4;

      then

       J4: x in [.b, c.] by J3;

      

       jj: ( dom f) = REAL by FUNCT_2:def 1;

      

       T1: x in ( dom g) by J4, jj, RELAT_1: 57;

      ( rng f) = REAL by FCONT_1: 55, A0;

      then

       S2: yy in ( rng f) by XREAL_0:def 1;

      set ff = (f qua Function " );

      (g . (ff . yy)) = (f . (ff . yy)) by FUNCT_1: 49, J4

      .= yy by A0, S2, FUNCT_1: 35;

      hence thesis by T1, FUNCT_1:def 3;

    end;

    theorem :: FUZNUM_1:13

    

     Hope5: (( AffineMap ( 0 , 0 )) . x) <> 1

    proof

      (( AffineMap ( 0 , 0 )) . x) = (( 0 * x) + 0 ) by FCONT_1:def 4

      .= 0 ;

      hence thesis;

    end;

    theorem :: FUZNUM_1:14

    (( AffineMap ( 0 ,1)) . b) = 1

    proof

      (( AffineMap ( 0 ,1)) . b) = (( 0 * b) + 1) by FCONT_1:def 4

      .= 1;

      hence thesis;

    end;

    theorem :: FUZNUM_1:15

    

     Kici1: for a be Real holds (( AffineMap ( 0 ,b)) . a) = b

    proof

      let a be Real;

      (( AffineMap ( 0 ,b)) . a) = (( 0 * a) + b) by FCONT_1:def 4

      .= b;

      hence thesis;

    end;

    begin

    reserve C for non empty set;

    definition

      let C be non empty set;

      mode FuzzySet of C is Membership_Func of C;

    end

    definition

      let C be non empty set;

      let F be FuzzySet of C;

      :: FUZNUM_1:def1

      attr F is normalized means ex x be Element of C st (F . x) = 1;

    end

    notation

      let C be non empty set;

      let F be FuzzySet of C;

      synonym F is normal for F is normalized;

    end

    notation

      let C be non empty set;

      let F be FuzzySet of C;

      antonym F is subnormal for F is normal;

    end

    definition

      let C be non empty set;

      let F be FuzzySet of C;

      :: FUZNUM_1:def2

      attr F is strictly-normalized means ex x be Element of C st (F . x) = 1 & for y be Element of C st (F . y) = 1 holds y = x;

    end

    registration

      let C be non empty set;

      cluster strictly-normalized -> normalized for FuzzySet of C;

      coherence ;

    end

    definition

      let C be non empty set;

      let F be FuzzySet of C;

      let alpha be Real;

      :: FUZNUM_1:def3

      func alpha -cut F -> Subset of C equals { x where x be Element of C : (F . x) >= alpha };

      coherence

      proof

        set H = { x where x be Element of C : (F . x) >= alpha };

        H c= C

        proof

          let y be object;

          assume y in H;

          then

          consider x be Element of C such that

           A1: y = x & (F . x) >= alpha;

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: FUZNUM_1:16

    

     AlphaCut1: for F be FuzzySet of C, alpha be Real holds (alpha -cut F) = (F " [.alpha, 1.])

    proof

      let F be FuzzySet of C, alpha be Real;

      thus (alpha -cut F) c= (F " [.alpha, 1.])

      proof

        let x be object;

        assume x in (alpha -cut F);

        then

        consider y be Element of C such that

         A1: x = y & (F . y) >= alpha;

        x in C by A1;

        then

         A2: x in ( dom F) by FUNCT_2:def 1;

        then (F . y) in [. 0 , 1.] by A1, PARTFUN1: 4;

        then 0 <= (F . y) & (F . y) <= 1 by XXREAL_1: 1;

        then (F . y) in [.alpha, 1.] by A1;

        hence thesis by A1, FUNCT_1:def 7, A2;

      end;

      let x be object;

      assume

       c2: x in (F " [.alpha, 1.]);

      then x in ( dom F) & (F . x) in [.alpha, 1.] by FUNCT_1:def 7;

      then alpha <= (F . x) & (F . x) <= 1 by XXREAL_1: 1;

      hence thesis by c2;

    end;

    registration

      let C;

      cluster ( UMF C) -> normalized;

      coherence

      proof

        ex x be Element of C st (( UMF C) . x) = 1

        proof

          take x = the Element of C;

          thus thesis by FUNCT_3:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      let C;

      cluster normalized for FuzzySet of C;

      existence

      proof

        take ( UMF C);

        thus thesis;

      end;

    end

    definition

      let C;

      let F be FuzzySet of C;

      :: FUZNUM_1:def4

      func Core F -> Subset of C equals { x where x be Element of C : (F . x) = 1 };

      coherence

      proof

        set H = { x where x be Element of C : (F . x) = 1 };

        H c= C

        proof

          let y be object;

          assume y in H;

          then

          consider x be Element of C such that

           A1: y = x & (F . x) = 1;

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: FUZNUM_1:17

    ( Core ( UMF C)) = C

    proof

      thus ( Core ( UMF C)) c= C;

      let x be object;

      assume x in C;

      then

      reconsider xx = x as Element of C;

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

      hence thesis;

    end;

    theorem :: FUZNUM_1:18

    

     CEmpty: ( Core ( EMF C)) = {}

    proof

      thus ( Core ( EMF C)) c= {}

      proof

        let x be object;

        assume x in ( Core ( EMF C));

        then

        consider xx be Element of C such that

         A1: x = xx & (( EMF C) . xx) = 1;

        thus thesis by A1, FUNCT_3:def 3;

      end;

      thus thesis;

    end;

    registration

      let C;

      cluster ( Core ( EMF C)) -> empty;

      coherence by CEmpty;

    end

    theorem :: FUZNUM_1:19

    

     CCounter: for F be FuzzySet of C holds ( Core F) = (F " {1})

    proof

      let F be FuzzySet of C;

      thus ( Core F) c= (F " {1})

      proof

        let x be object;

        assume x in ( Core F);

        then

        consider xx be Element of C such that

         A1: x = xx & (F . xx) = 1;

        

         A2: (F . xx) in {1} by TARSKI:def 1, A1;

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

        hence thesis by A1, FUNCT_1:def 7, A2;

      end;

      let x be object;

      assume

       a1: x in (F " {1});

      then

       A1: x in ( dom F) & (F . x) in {1} by FUNCT_1:def 7;

      reconsider xx = x as Element of C by a1;

      (F . xx) = 1 by A1, TARSKI:def 1;

      hence thesis;

    end;

    theorem :: FUZNUM_1:20

    for F be FuzzySet of C holds ( Core F) = (1 -cut F)

    proof

      let F be FuzzySet of C;

      (1 -cut F) = (F " [.1, 1.]) by AlphaCut1

      .= (F " {1}) by XXREAL_1: 17;

      hence thesis by CCounter;

    end;

    begin

    definition

      let F be FuzzySet of REAL ;

      :: FUZNUM_1:def5

      attr F is f-convex means for x1,x2 be Real, l be Real st 0 <= l & l <= 1 holds (F . ((l * x1) + ((1 - l) * x2))) >= ( min ((F . x1),(F . x2)));

    end

    

     UCon: ( UMF REAL ) is f-convex

    proof

      for x1,x2 be Real, l be Real st 0 <= l & l <= 1 holds (( UMF REAL ) . ((l * x1) + ((1 - l) * x2))) >= ( min ((( UMF REAL ) . x1),(( UMF REAL ) . x2)))

      proof

        let x1,x2 be Real, l be Real;

        set F = ( UMF REAL );

        assume 0 <= l & l <= 1;

        x1 in REAL & x2 in REAL by XREAL_0:def 1;

        then

         A1: (F . x1) = 1 & (F . x2) = 1 by FUNCT_3:def 3;

        ((l * x1) + ((1 - l) * x2)) in REAL by XREAL_0:def 1;

        hence thesis by A1, FUNCT_3:def 3;

      end;

      hence thesis;

    end;

    

     ECon: ( EMF REAL ) is f-convex

    proof

      for x1,x2 be Real, l be Real st 0 <= l & l <= 1 holds (( EMF REAL ) . ((l * x1) + ((1 - l) * x2))) >= ( min ((( EMF REAL ) . x1),(( EMF REAL ) . x2)))

      proof

        let x1,x2 be Real, l be Real;

        set F = ( EMF REAL );

        assume 0 <= l & l <= 1;

        

         A3: x1 in REAL & x2 in REAL by XREAL_0:def 1;

        

         A1: (F . x1) = {} & (F . x2) = {} by FUNCT_3:def 3, A3;

        ((l * x1) + ((1 - l) * x2)) in REAL by XREAL_0:def 1;

        hence thesis by A1, FUNCT_3:def 3;

      end;

      hence thesis;

    end;

    registration

      cluster ( UMF REAL ) -> f-convex;

      coherence by UCon;

      cluster ( EMF REAL ) -> f-convex;

      coherence by ECon;

    end

    definition

      let C be non empty set;

      let F be FuzzySet of C;

      :: FUZNUM_1:def6

      func height F -> ExtReal equals ( sup ( rng F));

      coherence ;

    end

    theorem :: FUZNUM_1:21

    

     HgtBnd: for F be FuzzySet of C holds 0 <= ( height F) & ( height F) <= 1

    proof

      let F be FuzzySet of C;

      

       B0: 0 is LowerBound of ( rng F)

      proof

        let x be ExtReal;

        assume x in ( rng F);

        then

        consider xx be object such that

         B1: xx in ( dom F) & x = (F . xx) by FUNCT_1:def 3;

        reconsider xx as Element of C by B1;

        thus thesis by B1, FUZZY_2: 1;

      end;

      

       b2: 1 is UpperBound of ( rng F)

      proof

        let x be ExtReal;

        assume x in ( rng F);

        then

        consider xx be object such that

         B1: xx in ( dom F) & x = (F . xx) by FUNCT_1:def 3;

        reconsider xx as Element of C by B1;

        thus thesis by B1, FUZZY_2: 1;

      end;

      ( inf ( rng F)) <= ( sup ( rng F)) by XXREAL_2: 40;

      hence thesis by b2, B0, XXREAL_2:def 4, XXREAL_2:def 3;

    end;

    theorem :: FUZNUM_1:22

    for F be FuzzySet of C st F is normalized holds ( height F) = 1

    proof

      let F be FuzzySet of C;

      assume F is normalized;

      then

      consider x be Element of C such that

       A1: (F . x) = 1;

      x in C;

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

      then

       A2: 1 <= ( height F) by XXREAL_2: 4, FUNCT_1: 3, A1;

      ( height F) <= 1 by HgtBnd;

      hence ( height F) = 1 by A2, XXREAL_0: 1;

    end;

    begin

    theorem :: FUZNUM_1:23

    for f,g be PartFunc of REAL , REAL st f is continuous & g is continuous & ex x be object st (( dom f) /\ ( dom g)) = {x} & for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x) holds ex h be PartFunc of REAL , REAL st h = (f +* g) & for x be Real st x in (( dom f) /\ ( dom g)) holds h is_continuous_in x

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume

       A1: f is continuous & g is continuous & ex x be object st (( dom f) /\ ( dom g)) = {x} & for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x);

      reconsider h = (f +* g) as PartFunc of REAL , REAL ;

      take h;

      thus h = (f +* g);

      let x be Real;

      

       J2: (h | ( dom f)) = ((g +* f) | ( dom f)) by FUNCT_4: 34, PARTFUN1:def 4, A1

      .= f;

      assume x in (( dom f) /\ ( dom g));

      then

       ZR: x in ( dom f) & x in ( dom g) by XBOOLE_0:def 4;

      then

       JJ: x in ( dom h) by FUNCT_4: 12;

      for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom h) & |.(x1 - x).| < s holds |.((h . x1) - (h . x)).| < r

      proof

        let r be Real;

        set hf = (h | ( dom f));

        set hg = (h | ( dom g));

        

         SF: x in ( dom hf) by RELAT_1: 57, ZR, JJ;

        

         Sf: x in ( dom hg) by ZR;

        assume

         R0: 0 < r;

        consider s2 be Real such that

         SB: 0 < s2 & for x1 be Real st x1 in ( dom hf) & |.(x1 - x).| < s2 holds |.((hf . x1) - (hf . x)).| < (r / 2) by J2, ZR, A1, FCONT_1: 3, R0;

        consider s1 be Real such that

         Sb: 0 < s1 & for x1 be Real st x1 in ( dom hg) & |.(x1 - x).| < s1 holds |.((hg . x1) - (hg . x)).| < (r / 2) by FCONT_1: 3, ZR, A1, R0;

        take s = ( min (s2,s1));

        thus 0 < s by SB, Sb, XXREAL_0: 15;

        

         SS: (r / 2) < r by XREAL_1: 216, R0;

        let x1 be Real;

        assume

         SC: x1 in ( dom h) & |.(x1 - x).| < s;

        per cases by FUNCT_4: 12;

          suppose

           ZT: x1 in ( dom f) & x1 in ( dom g);

          

           i1: x1 in ( dom h) by FUNCT_4: 12, ZT;

          then

           I1: x1 in ( dom hf) by ZT, RELAT_1: 57;

          s <= s2 by XXREAL_0: 17;

          then |.(x1 - x).| < s2 by XXREAL_0: 2, SC;

          then

           SD: |.((hf . x1) - (hf . x)).| < (r / 2) by SB, i1, ZT, RELAT_1: 57;

          

           s1: (hf . x1) = (h . x1) by FUNCT_1: 47, I1;

          (hf . x) = (h . x) by FUNCT_1: 47, SF;

          hence thesis by SS, XXREAL_0: 2, SD, s1;

        end;

          suppose

           ZT: x1 in ( dom f) & not x1 in ( dom g);

          then

           i1: x1 in ( dom h) by FUNCT_4: 12;

          then

           I1: x1 in ( dom hf) by ZT, RELAT_1: 57;

          s <= s2 by XXREAL_0: 17;

          then |.(x1 - x).| < s2 by XXREAL_0: 2, SC;

          then

           SD: |.((hf . x1) - (hf . x)).| < (r / 2) by SB, i1, ZT, RELAT_1: 57;

          

           s1: (hf . x1) = (h . x1) by FUNCT_1: 47, I1;

          (hf . x) = (h . x) by FUNCT_1: 47, SF;

          hence thesis by SS, XXREAL_0: 2, SD, s1;

        end;

          suppose

           P1: x1 in ( dom g);

          x1 in ( dom hg) by P1;

          then

           P2: (h . x1) = (hg . x1) by FUNCT_1: 47;

          

           P3: (h . x) = (hg . x) by FUNCT_1: 47, Sf;

          s <= s1 by XXREAL_0: 17;

          then |.(x1 - x).| < s1 by XXREAL_0: 2, SC;

          then |.((hg . x1) - (hg . x)).| < (r / 2) by Sb, P1;

          hence thesis by SS, XXREAL_0: 2, P3, P2;

        end;

      end;

      hence thesis by FCONT_1: 3;

    end;

    theorem :: FUZNUM_1:24

    

     LemGlue: for f,g be PartFunc of REAL , REAL st f is continuous non empty & g is continuous non empty & (ex a,b,c be Real st ( dom f) = [.a, b.] & ( dom g) = [.b, c.]) & f tolerates g holds ex h be PartFunc of REAL , REAL st h = (f +* g) & for x be Real st x in ( dom h) holds h is_continuous_in x

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume

       A1: f is continuous non empty & g is continuous non empty & (ex a,b,c be Real st ( dom f) = [.a, b.] & ( dom g) = [.b, c.]) & f tolerates g;

      reconsider ff = f, gg = g as non empty continuous PartFunc of REAL , REAL by A1;

      consider a,b,c be Real such that

       AB: ( dom f) = [.a, b.] & ( dom g) = [.b, c.] by A1;

      ( dom ff) <> {} & ( dom gg) <> {} ;

      then

       Ab: a <= b & b <= c by XXREAL_1: 29, AB;

      

       AA: (( dom f) /\ ( dom g)) = {b} by XXREAL_1: 418, Ab, AB;

      reconsider h = (f +* g) as PartFunc of REAL , REAL ;

      take h;

      thus h = (f +* g);

      let x be Real;

      

       J2: (h | ( dom f)) = ((g +* f) | ( dom f)) by FUNCT_4: 34, A1

      .= f;

      assume

       JJ: x in ( dom h);

      per cases by FUNCT_4: 12;

        suppose

         J1: x in ( dom f);

        set hf = (h | ( dom f));

        set hg = (h | ( dom g));

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom h) & |.(x1 - x).| < s holds |.((h . x1) - (h . x)).| < r

        proof

          let r be Real;

          ( dom f) c= ( dom h) & ( dom g) c= ( dom h) by FUNCT_4: 10;

          then

           XX: ( dom hf) = ( dom f) & ( dom hg) = ( dom g) by RELAT_1: 62;

          

           SF: x in ( dom hf) by RELAT_1: 57, J1, JJ;

          assume

           R0: 0 < r;

          then

          consider s2 be Real such that

           SB: 0 < s2 & for x1 be Real st x1 in ( dom hf) & |.(x1 - x).| < s2 holds |.((hf . x1) - (hf . x)).| < (r / 2) by J1, J2, A1, FCONT_1: 3;

          

           KK: b in (( dom f) /\ ( dom g)) by AA, TARSKI:def 1;

          then

           KA: b in ( dom f) & b in ( dom g) by XBOOLE_0:def 4;

          

           KI: b in ( dom hf) & b in ( dom hg) by XX, XBOOLE_0:def 4, KK;

          consider s1 be Real such that

           Sb: 0 < s1 & for x1 be Real st x1 in ( dom hg) & |.(x1 - b).| < s1 holds |.((hg . x1) - (hg . b)).| < (r / 2) by FCONT_1: 3, R0, A1, KA;

          take s = ( min (s2,s1));

          thus 0 < s by SB, Sb, XXREAL_0: 15;

          

           SS: (r / 2) < r by XREAL_1: 216, R0;

          let x1 be Real;

          assume

           SC: x1 in ( dom h) & |.(x1 - x).| < s;

          s <= s2 by XXREAL_0: 17;

          then

           H1: |.(x1 - x).| < s2 by XXREAL_0: 2, SC;

          per cases by FUNCT_4: 12, SC;

            suppose

             ZT: x1 in ( dom f);

            then

             I1: x1 in ( dom hf) by RELAT_1: 57, SC;

            

             SD: |.((hf . x1) - (hf . x)).| < (r / 2) by SB, ZT, H1, RELAT_1: 57, SC;

            

             s1: (hf . x1) = (h . x1) by FUNCT_1: 47, I1;

             |.((h . x1) - (h . x)).| < (r / 2) by SD, s1, FUNCT_1: 47, SF;

            hence thesis by SS, XXREAL_0: 2;

          end;

            suppose

             P1: x1 in ( dom g);

            then x1 in ( dom hg);

            then

             P2: (h . x1) = (hg . x1) by FUNCT_1: 47;

            

             P3: (h . x) = (hf . x) by FUNCT_1: 47, SF;

            s <= s1 by XXREAL_0: 17;

            then

             P6: |.(x1 - x).| < s1 by XXREAL_0: 2, SC;

            

             WA: (hg . b) = (hf . b) by J2, KK, A1, PARTFUN1:def 4;

            

             M3: (x + 0 ) <= b by XXREAL_1: 1, J1, AB;

            

             M7: b <= x1 & x1 <= c by XXREAL_1: 1, P1, AB;

            

             m0: (x + 0 ) <= x1 by M7, XXREAL_0: 2, M3;

            (b + 0 ) <= x1 by XXREAL_1: 1, P1, AB;

            then

             M1: |.(x1 - b).| = (x1 - b) by ABSVALUE:def 1, XREAL_1: 19;

            

             M2: |.(b - x).| = (b - x) by ABSVALUE:def 1, M3, XREAL_1: 19;

            

             M8: |.(x1 - x).| = ( |.(x1 - b).| + |.(b - x).|) by M1, M2, m0, ABSVALUE:def 1, XREAL_1: 19;

            then |.(x1 - b).| <= |.(x1 - x).| by COMPLEX1: 46, XREAL_1: 31;

            then |.(x1 - b).| < s1 by P6, XXREAL_0: 2;

            then

             KJ: |.((hg . x1) - (hg . b)).| < (r / 2) by Sb, P1;

             |.(b - x).| <= |.(x1 - x).| by M8, XREAL_1: 31, COMPLEX1: 46;

            then |.(b - x).| < s2 by H1, XXREAL_0: 2;

            then |.((hf . b) - (hf . x)).| < (r / 2) by SB, KI;

            then

             WW: ( |.((hg . x1) - (hg . b)).| + |.((hf . b) - (hf . x)).|) < ((r / 2) + (r / 2)) by KJ, XREAL_1: 8;

             |.((hg . x1) - (hf . x)).| <= ( |.((hg . x1) - (hg . b)).| + |.((hg . b) - (hf . x)).|) by COMPLEX1: 63;

            hence thesis by P2, P3, WA, XXREAL_0: 2, WW;

          end;

        end;

        hence thesis by FCONT_1: 3;

      end;

        suppose

         J1: x in ( dom g);

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom h) & |.(x1 - x).| < s holds |.((h . x1) - (h . x)).| < r

        proof

          let r be Real;

          set hf = (h | ( dom f));

          set hg = (h | ( dom g));

          ( dom f) c= ( dom h) & ( dom g) c= ( dom h) by FUNCT_4: 10;

          then

           XX: ( dom hf) = ( dom f) & ( dom hg) = ( dom g) by RELAT_1: 62;

          

           SF: x in ( dom hg) by J1;

          assume

           R0: 0 < r;

          then

          consider s2 be Real such that

           SB: 0 < s2 & for x1 be Real st x1 in ( dom hg) & |.(x1 - x).| < s2 holds |.((hg . x1) - (hg . x)).| < (r / 2) by J1, FCONT_1: 3, A1;

          

           KK: b in (( dom f) /\ ( dom g)) by AA, TARSKI:def 1;

          then

           KA: b in ( dom f) & b in ( dom g) by XBOOLE_0:def 4;

          

           KI: b in ( dom hf) & b in ( dom hg) by XX, KK, XBOOLE_0:def 4;

          consider s1 be Real such that

           Sb: 0 < s1 & for x1 be Real st x1 in ( dom hf) & |.(x1 - b).| < s1 holds |.((hf . x1) - (hf . b)).| < (r / 2) by FCONT_1: 3, R0, J2, A1, KA;

          take s = ( min (s2,s1));

          thus 0 < s by SB, Sb, XXREAL_0: 15;

          

           SS: (r / 2) < r by XREAL_1: 216, R0;

          let x1 be Real;

          assume

           SC: x1 in ( dom h) & |.(x1 - x).| < s;

          s <= s2 by XXREAL_0: 17;

          then

           H1: |.(x1 - x).| < s2 by XXREAL_0: 2, SC;

          per cases by FUNCT_4: 12, SC;

            suppose

             ZT: x1 in ( dom g);

            then

             I1: x1 in ( dom hg);

            

             SD: |.((hg . x1) - (hg . x)).| < (r / 2) by SB, ZT, H1;

            

             s1: (hg . x1) = (h . x1) by FUNCT_1: 47, I1;

             |.((h . x1) - (h . x)).| < (r / 2) by SD, s1, FUNCT_1: 47, SF;

            hence thesis by SS, XXREAL_0: 2;

          end;

            suppose

             P1: x1 in ( dom f);

            then x1 in ( dom hf) by RELAT_1: 57, SC;

            then

             P2: (h . x1) = (hf . x1) by FUNCT_1: 47;

            

             P3: (h . x) = (hg . x) by FUNCT_1: 47, SF;

            s <= s1 by XXREAL_0: 17;

            then |.(x1 - x).| < s1 by XXREAL_0: 2, SC;

            then

             P6: |.(x - x1).| < s1 by COMPLEX1: 60;

            

             WA: (hg . b) = (hf . b) by J2, KK, A1, PARTFUN1:def 4;

            

             M3: (x - 0 ) >= b by XXREAL_1: 1, J1, AB;

            

             M7: a <= x1 & x1 <= b by XXREAL_1: 1, P1, AB;

            

             m0: (x1 + 0 ) <= x by M7, XXREAL_0: 2, M3;

            (b - 0 ) >= x1 by XXREAL_1: 1, P1, AB;

            then

             M1: |.(b - x1).| = (b - x1) by ABSVALUE:def 1, XREAL_1: 11;

            

             M2: |.(x - b).| = (x - b) by ABSVALUE:def 1, M3, XREAL_1: 11;

            

             M8: |.(x - x1).| = ( |.(b - x1).| + |.(x - b).|) by M1, M2, m0, ABSVALUE:def 1, XREAL_1: 19;

            then |.(b - x1).| <= |.(x - x1).| by COMPLEX1: 46, XREAL_1: 31;

            then |.(b - x1).| < s1 by P6, XXREAL_0: 2;

            then |.(x1 - b).| < s1 by COMPLEX1: 60;

            then

             KJ: |.((hf . x1) - (hf . b)).| < (r / 2) by Sb, P1, RELAT_1: 57, SC;

            

             LK: |.(b - x).| = |.(x - b).| by COMPLEX1: 60;

             |.(x - b).| <= |.(x - x1).| by M8, XREAL_1: 31, COMPLEX1: 46;

            then |.(b - x).| <= |.(x1 - x).| by COMPLEX1: 60, LK;

            then |.(b - x).| < s2 by H1, XXREAL_0: 2;

            then |.((hg . b) - (hg . x)).| < (r / 2) by SB, KI;

            then

             WW: ( |.((hf . x1) - (hf . b)).| + |.((hg . b) - (hg . x)).|) < ((r / 2) + (r / 2)) by KJ, XREAL_1: 8;

             |.((hf . x1) - (hg . x)).| <= ( |.((hf . x1) - (hf . b)).| + |.((hf . b) - (hg . x)).|) by COMPLEX1: 63;

            hence thesis by P2, P3, WA, XXREAL_0: 2, WW;

          end;

        end;

        hence thesis by FCONT_1: 3;

      end;

    end;

    theorem :: FUZNUM_1:25

    

     Glue: for f,g be PartFunc of REAL , REAL st f is continuous non empty & g is continuous non empty & (ex a,b,c be Real st ( dom f) = [.a, b.] & ( dom g) = [.b, c.]) & f tolerates g holds (f +* g) is continuous

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume f is continuous non empty & g is continuous non empty & (ex a,b,c be Real st ( dom f) = [.a, b.] & ( dom g) = [.b, c.]) & f tolerates g;

      then

      consider h be PartFunc of REAL , REAL such that

       A2: h = (f +* g) & for x be Real st x in ( dom h) holds h is_continuous_in x by LemGlue;

      thus thesis by A2;

    end;

    theorem :: FUZNUM_1:26

    

     Asi1: for f,g be PartFunc of REAL , REAL st g is non empty & f = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, b.[)) & ( dom g) = [.a, b.] & (g . a) = 0 & (g . b) = 0 holds f tolerates g

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume

       A1: g is non empty & f = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, b.[)) & ( dom g) = [.a, b.] & (g . a) = 0 & (g . b) = 0 ;

      ( REAL \ ].a, b.[) c= REAL ;

      then ( REAL \ ].a, b.[) c= ( dom ( AffineMap ( 0 , 0 ))) by FUNCT_2:def 1;

      

      then

       A2: ( dom f) = ( REAL \ ].a, b.[) by RELAT_1: 62, A1

      .= ( ]. -infty , a.] \/ [.b, +infty .[) by XXREAL_1: 398;

      for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x)

      proof

        let x be object;

        

         K2: b < +infty by XXREAL_0: 9, XREAL_0:def 1;

        

         K3: -infty < a by XXREAL_0: 12, XREAL_0:def 1;

        assume

         P1: x in (( dom f) /\ ( dom g));

        then x in (( [.a, b.] /\ ]. -infty , a.]) \/ ( [.a, b.] /\ [.b, +infty .[)) by XBOOLE_1: 23, A1, A2;

        then x in ( {a} \/ ( [.a, b.] /\ [.b, +infty .[)) by XXREAL_1: 417, A1, XXREAL_1: 29, K3;

        then x in ( {a} \/ {b}) by XXREAL_1: 416, A1, XXREAL_1: 29, K2;

        then x in {a, b} by ENUMSET1: 1;

        then

         W1: (g . x) = 0 by A1, TARSKI:def 2;

        reconsider xx = x as Real by P1;

        x in ( dom f) by P1, XBOOLE_0:def 4;

        then (f . x) = (( AffineMap ( 0 , 0 )) . xx) by A1, FUNCT_1: 47;

        hence thesis by Kici1, W1;

      end;

      hence thesis by PARTFUN1:def 4;

    end;

    theorem :: FUZNUM_1:27

    

     Kluczyk: for f,g be PartFunc of REAL , REAL st g is continuous non empty & f = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, b.[)) & ( dom g) = [.a, b.] & (g . a) = 0 & (g . b) = 0 holds ex h be PartFunc of REAL , REAL st h = (f +* g) & for x be Real st x in ( dom h) holds h is_continuous_in x

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume

       A1: g is continuous non empty & f = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, b.[)) & ( dom g) = [.a, b.] & (g . a) = 0 & (g . b) = 0 ;

      then

       KK: f tolerates g by Asi1;

      set c = b;

      take h = (f +* g);

      thus h = (f +* g);

      let x be Real;

      

       U1: -infty < a by XXREAL_0: 12, XREAL_0:def 1;

      

       U3: b < +infty by XXREAL_0: 9, XREAL_0:def 1;

      ( REAL \ ].a, b.[) c= REAL ;

      then ( REAL \ ].a, b.[) c= ( dom ( AffineMap ( 0 , 0 ))) by FUNCT_2:def 1;

      then

       S1: ( dom f) = ( REAL \ ].a, b.[) by A1, RELAT_1: 62;

      

       aa: (( REAL \ ].a, b.[) /\ [.a, b.]) = (( ]. -infty , a.] \/ [.b, +infty .[) /\ [.a, b.]) by XXREAL_1: 398

      .= (( ]. -infty , a.] /\ [.a, b.]) \/ ( [.b, +infty .[ /\ [.a, b.])) by XBOOLE_1: 23

      .= ( {a} \/ ( [.b, +infty .[ /\ [.a, b.])) by XXREAL_1: 417, U1, XXREAL_1: 29, A1

      .= ( {a} \/ {b}) by XXREAL_1: 416, XXREAL_1: 29, A1, U3

      .= {a, b} by ENUMSET1: 1;

      a in (( dom f) /\ ( dom g)) by aa, S1, A1, TARSKI:def 2;

      then

       sx: a in ( dom f) & a in ( dom g) by XBOOLE_0:def 4;

      

       nn: (f . a) = (( AffineMap ( 0 , 0 )) . a) by FUNCT_1: 47, A1, sx

      .= (( 0 * a) + 0 ) by FCONT_1:def 4

      .= 0 ;

      b in (( dom f) /\ ( dom g)) by aa, S1, A1, TARSKI:def 2;

      then

       sy: b in ( dom f) & b in ( dom g) by XBOOLE_0:def 4;

      

      then

       mn: (f . b) = (( AffineMap ( 0 , 0 )) . b) by FUNCT_1: 47, A1

      .= (( 0 * b) + 0 ) by FCONT_1:def 4

      .= 0 ;

      

       Z7: ( dom f) = ( ]. -infty , a.] \/ [.b, +infty .[) by S1, XXREAL_1: 398;

      

       Z8: ]. -infty , a.[ c= ]. -infty , a.] by XXREAL_1: 21;

      

       xz: ]. -infty , a.] c= ( dom f) by XBOOLE_1: 7, Z7;

      then

       Z6: ]. -infty , a.[ c= ( dom f) by Z8;

      

       z8: ].b, +infty .[ c= [.b, +infty .[ by XXREAL_1: 22;

      

       wz: [.b, +infty .[ c= ( dom f) by XBOOLE_1: 7, Z7;

      then

       z6: ].b, +infty .[ c= ( dom f) by z8;

      assume x in ( dom h);

      then

       R1: x in ( dom f) or x in ( dom g) by FUNCT_4: 12;

      set xx0 = x;

      

       b2: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      

       b1: ].a, b.[ c= ( dom g) by A1, XXREAL_1: 25;

      x in ]. -infty , a.] or x in [.b, +infty .[ or x in [.a, b.] by A1, R1, Z7, XBOOLE_0:def 3;

      then x in ( ]. -infty , a.[ \/ {a}) or x in [.b, +infty .[ or x in [.a, b.] by XXREAL_1: 423;

      then x in ]. -infty , a.[ or x in {a} or x in [.b, +infty .[ or x in [.a, b.] by XBOOLE_0:def 3;

      then x in ]. -infty , a.[ or x = a or x in ( {b} \/ ].b, +infty .[) or x in [.a, b.] by XXREAL_1: 427, TARSKI:def 1;

      then x in ]. -infty , a.[ or x = a or x in {b} or x in ].b, +infty .[ or x in [.a, b.] by XBOOLE_0:def 3;

      then x in ]. -infty , a.[ or x = a or x = b or x in ].b, +infty .[ or x in ( {a, b} \/ ].a, b.[) by XXREAL_1: 29, XXREAL_1: 128, TARSKI:def 1;

      then x in ]. -infty , a.[ or x = a or x = b or x in ].b, +infty .[ or x in {a, b} or x in {a, b} or x in ].a, b.[ by XBOOLE_0:def 3;

      per cases by TARSKI:def 2;

        suppose

         FT: x = a;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom h) & |.(x1 - x).| < s holds |.((h . x1) - (h . x)).| < r

        proof

          let r be Real;

          assume

           H1: 0 < r;

          then

          consider s1 be Real such that

           WW: 0 < s1 & for x1 be Real st x1 in ( dom g) & |.(x1 - x).| < s1 holds |.((g . x1) - (g . x)).| < r by FCONT_1: 3, A1, sx, FT;

          consider s2 be Real such that

           W1: 0 < s2 & for x1 be Real st x1 in ( dom f) & |.(x1 - x).| < s2 holds |.((f . x1) - (f . x)).| < r by FCONT_1: 3, H1, FCONT_1:def 2, A1, sx, FT;

          take s = ( min (s1,s2));

          thus 0 < s by WW, W1, XXREAL_0: 15;

          

           O2: s <= s1 & s <= s2 by XXREAL_0: 17;

          let x1 be Real;

          assume

           O1: x1 in ( dom h) & |.(x1 - x).| < s;

          per cases by FUNCT_4: 12;

            suppose

             W2: x1 in ( dom f) & not x1 in ( dom g);

            then

             W3: (h . x1) = (f . x1) by FUNCT_4: 11;

            

             W4: (h . x) = (f . x) by A1, FT, nn, FUNCT_4: 13, sx;

             |.(x1 - x).| < s2 by O1, O2, XXREAL_0: 2;

            hence |.((h . x1) - (h . x)).| < r by W3, W4, W1, W2;

          end;

            suppose

             W2: x1 in ( dom f) & x1 in ( dom g);

            then

             W3: (h . x1) = (g . x1) by FUNCT_4: 13;

            

             W4: (h . x) = (g . x) by FUNCT_4: 13, sx, FT;

             |.(x1 - x).| < s1 by O1, O2, XXREAL_0: 2;

            hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW;

          end;

            suppose

             W2: x1 in ( dom g);

            then

             W3: (h . x1) = (g . x1) by FUNCT_4: 13;

            

             W4: (h . x) = (g . x) by FUNCT_4: 13, FT, sx;

             |.(x1 - x).| < s1 by O1, O2, XXREAL_0: 2;

            hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW;

          end;

        end;

        hence thesis by FCONT_1: 3;

      end;

        suppose

         FT: x = b;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom h) & |.(x1 - x).| < s holds |.((h . x1) - (h . x)).| < r

        proof

          let r be Real;

          assume

           H1: 0 < r;

          then

          consider s1 be Real such that

           WW: 0 < s1 & for x1 be Real st x1 in ( dom g) & |.(x1 - x).| < s1 holds |.((g . x1) - (g . x)).| < r by FCONT_1: 3, A1, sy, FT;

          consider s2 be Real such that

           W1: 0 < s2 & for x1 be Real st x1 in ( dom f) & |.(x1 - x).| < s2 holds |.((f . x1) - (f . x)).| < r by FCONT_1: 3, H1, FCONT_1:def 2, A1, sy, FT;

          take s = ( min (s1,s2));

          thus 0 < s by WW, W1, XXREAL_0: 15;

          

           O2: s <= s1 & s <= s2 by XXREAL_0: 17;

          let x1 be Real;

          assume

           O1: x1 in ( dom h) & |.(x1 - x).| < s;

          per cases by FUNCT_4: 12;

            suppose

             W2: x1 in ( dom f) & not x1 in ( dom g);

            then

             W3: (h . x1) = (f . x1) by FUNCT_4: 11;

            

             W4: (h . x) = (f . x) by mn, A1, FT, sy, FUNCT_4: 13;

             |.(x1 - x).| < s2 by O1, O2, XXREAL_0: 2;

            hence |.((h . x1) - (h . x)).| < r by W3, W4, W1, W2;

          end;

            suppose

             W2: x1 in ( dom f) & x1 in ( dom g);

            then

             W3: (h . x1) = (g . x1) by FUNCT_4: 13;

            

             W4: (h . x) = (g . x) by FUNCT_4: 13, sy, FT;

             |.(x1 - x).| < s1 by O1, O2, XXREAL_0: 2;

            hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW;

          end;

            suppose

             W2: x1 in ( dom g);

            then

             W3: (h . x1) = (g . x1) by FUNCT_4: 13;

            

             W4: (h . x) = (g . x) by FUNCT_4: 13, FT, sy;

             |.(x1 - x).| < s1 by O1, O2, XXREAL_0: 2;

            hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW;

          end;

        end;

        hence thesis by FCONT_1: 3;

      end;

        suppose

         B0: xx0 in ]. -infty , a.[;

        for N1 be Neighbourhood of (h . xx0) holds ex N be Neighbourhood of xx0 st for x1 be Real st x1 in ( dom h) & x1 in N holds (h . x1) in N1

        proof

          let N1 be Neighbourhood of (h . xx0);

          set r = (h . xx0);

          reconsider N2 = N1 as Neighbourhood of (f . xx0) by B0, Z8, xz, FUNCT_4: 15, KK;

          f is continuous by A1;

          then

          consider Nx be Neighbourhood of xx0 such that

           D0: for x1 be Real st x1 in ( dom f) & x1 in Nx holds (f . x1) in N2 by FCONT_1: 4, B0, Z6;

          set rr = (a - xx0);

          

           Zz: (xx0 + 0 ) < a by B0, XXREAL_1: 233;

          then

           Z1: rr > 0 by XREAL_1: 20;

          set rr2 = (rr / 2);

          set P1 = ].(xx0 - rr2), (xx0 + rr2).[;

          (xx0 / 2) < (a / 2) by Zz, XREAL_1: 74;

          then

           z5: ((xx0 / 2) + (a / 2)) < ((a / 2) + (a / 2)) by XREAL_1: 8;

          P1 c= ]. -infty , a.[ by XXREAL_1: 263, z5;

          then

           Y1: P1 c= ( dom f) by Z8, xz;

          reconsider P1 as Neighbourhood of xx0 by Z1, RCOMP_1:def 6;

          consider N be Neighbourhood of xx0 such that

           Y2: N c= Nx & N c= P1 by RCOMP_1: 17;

          take N;

          let x1 be Real;

          assume

           D1: x1 in ( dom h) & x1 in N;

          then (f . x1) in N2 by D0, Y2, Y1;

          hence thesis by FUNCT_4: 15, Y2, Y1, D1, KK;

        end;

        hence thesis by FCONT_1: 4;

      end;

        suppose

         B0: xx0 in ].a, b.[;

        for N1 be Neighbourhood of (h . xx0) holds ex N be Neighbourhood of xx0 st for x1 be Real st x1 in ( dom h) & x1 in N holds (h . x1) in N1

        proof

          let N1 be Neighbourhood of (h . xx0);

          set r = (h . xx0);

          reconsider N2 = N1 as Neighbourhood of (g . xx0) by B0, A1, b2, FUNCT_4: 13;

          consider Nx be Neighbourhood of xx0 such that

           D0: for x1 be Real st x1 in ( dom g) & x1 in Nx holds (g . x1) in N2 by FCONT_1: 4, B0, b2, A1;

          set rr = ( min ((xx0 - a),(b - xx0)));

          

           Zw: a < xx0 & xx0 < b by B0, XXREAL_1: 4;

          (a - a) < (xx0 - a) & (b - xx0) > (xx0 - xx0) by XREAL_1: 14, Zw;

          then

           Z1: rr > 0 by XXREAL_0: 15;

          set rr2 = (rr / 2);

          set P1 = ].(xx0 - rr2), (xx0 + rr2).[;

          

           u1: rr2 < rr by Z1, XREAL_1: 216;

          

           u2: rr <= (b - xx0) by XXREAL_0: 17;

          

           u3: (xx0 + rr2) < (xx0 + rr) by u1, XREAL_1: 8;

          (xx0 + rr) <= (xx0 + (b - xx0)) by u2, XREAL_1: 7;

          then

           Z5: (xx0 + rr2) < b by u3, XXREAL_0: 2;

          rr <= (xx0 - a) by XXREAL_0: 17;

          then rr2 < (xx0 - a) by XXREAL_0: 2, u1;

          then

           h1: (xx0 - rr2) > (xx0 - (xx0 - a)) by XREAL_1: 15;

          

           y1: P1 c= ].a, b.[ by XXREAL_1: 46, Z5, h1;

          reconsider P1 as Neighbourhood of xx0 by Z1, RCOMP_1:def 6;

          consider N be Neighbourhood of xx0 such that

           Y2: N c= Nx & N c= P1 by RCOMP_1: 17;

          

           XX: N c= ( dom g) by Y2, y1, b1;

          take N;

          let x1 be Real;

          assume

           D1: x1 in ( dom h) & x1 in N;

          x1 in Nx & x1 in ( dom g) by Y2, y1, b1, D1;

          then (g . x1) in N2 by D0;

          hence thesis by FUNCT_4: 13, XX, D1;

        end;

        hence thesis by FCONT_1: 4;

      end;

        suppose

         B0: xx0 in ].b, +infty .[;

        for N1 be Neighbourhood of (h . xx0) holds ex N be Neighbourhood of xx0 st for x1 be Real st x1 in ( dom h) & x1 in N holds (h . x1) in N1

        proof

          let N1 be Neighbourhood of (h . xx0);

          set r = (h . xx0);

          reconsider N2 = N1 as Neighbourhood of (f . xx0) by B0, z6, FUNCT_4: 15, A1, Asi1;

          

           T1: f is continuous by A1;

          consider Nx be Neighbourhood of xx0 such that

           D0: for x1 be Real st x1 in ( dom f) & x1 in Nx holds (f . x1) in N2 by FCONT_1: 4, B0, z6, T1;

          set rr = (xx0 - b);

          

           Zz: (b + 0 ) < xx0 by B0, XXREAL_1: 235;

          then

           Z1: rr > 0 by XREAL_1: 20;

          set rr2 = (rr / 2);

          set P1 = ].(xx0 - rr2), (xx0 + rr2).[;

          

           Z3: (b / 2) < (xx0 / 2) by Zz, XREAL_1: 74;

          ((xx0 / 2) + (b / 2)) > ((b / 2) + (b / 2)) by Z3, XREAL_1: 8;

          then P1 c= ].b, +infty .[ by XXREAL_1: 247;

          then

           Y1: P1 c= ( dom f) by z8, wz;

          reconsider P1 as Neighbourhood of xx0 by Z1, RCOMP_1:def 6;

          consider N be Neighbourhood of xx0 such that

           Y2: N c= Nx & N c= P1 by RCOMP_1: 17;

          take N;

          let x1 be Real;

          assume

           D1: x1 in ( dom h) & x1 in N;

          then (f . x1) in N2 by D0, Y2, Y1;

          hence thesis by FUNCT_4: 15, Y2, Y1, D1, KK;

        end;

        hence thesis by FCONT_1: 4;

      end;

    end;

    theorem :: FUZNUM_1:28

    for f,g be PartFunc of REAL , REAL st g is continuous non empty & f = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, b.[)) & ( dom g) = [.a, b.] & (g . a) = 0 & (g . b) = 0 holds (f +* g) is continuous

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume g is continuous non empty & f = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, b.[)) & ( dom g) = [.a, b.] & (g . a) = 0 & (g . b) = 0 ;

      then

      consider h be PartFunc of REAL , REAL such that

       A2: h = (f +* g) & for x be Real st x in ( dom h) holds h is_continuous_in x by Kluczyk;

      thus thesis by A2;

    end;

    registration

      cluster non trivial closed_interval closed for Subset of REAL ;

      existence

      proof

        take A = [. 0 , 1.];

         0 in A & 1 in A;

        hence thesis by MEASURE5:def 3, ZFMISC_1:def 10;

      end;

    end

    begin

    definition

      let a,b,c be Real;

      assume that

       Z1: a < b and

       Z2: b < c;

      :: FUZNUM_1:def7

      func TriangularFS (a,b,c) -> FuzzySet of REAL equals

      : TrDef: (((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) +* (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.]));

      coherence

      proof

        

         k1: (a + 0 ) < b by Z1;

        

         k2: (b + 0 ) < c by Z2;

        set f1 = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)), f2 = (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.]), f3 = (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.]);

        set f = ((f1 +* f2) +* f3);

        ( REAL \ ].a, c.[) <> {} by RealNon, Z1, Z2, XXREAL_0: 2;

        then

         L1: ( rng f1) = { 0 } by Andr1a;

        

         L2: ( rng f2) = [. 0 , 1.] by k1, Hope1, XREAL_1: 20;

        

         L3: ( rng f3) = [. 0 , 1.] by Hope2a, k2, XREAL_1: 20;

        ( rng (f1 +* f2)) c= (( rng f1) \/ ( rng f2)) by FUNCT_4: 17;

        then

         L5: (( rng (f1 +* f2)) \/ ( rng f3)) c= (( { 0 } \/ [. 0 , 1.]) \/ ( rng f3)) by XBOOLE_1: 13, L1, L2;

        

         l6: ( rng f) c= (( rng (f1 +* f2)) \/ ( rng f3)) by FUNCT_4: 17;

         [. 0 , 0 .] c= [. 0 , 1.] by XXREAL_1: 34;

        then { 0 } c= [. 0 , 1.] by XXREAL_1: 17;

        then ( { 0 } \/ [. 0 , 1.]) = [. 0 , 1.] by XBOOLE_1: 12;

        then

         I3: ( rng f) c= [. 0 , 1.] by l6, L3, L5;

        

         I5: ( dom f) = (( dom (f1 +* f2)) \/ ( dom f3)) by FUNCT_4:def 1

        .= ((( dom f1) \/ ( dom f2)) \/ ( dom f3)) by FUNCT_4:def 1;

        ( REAL \ ].a, c.[) c= REAL ;

        then

         i7: ( REAL \ ].a, c.[) c= ( dom ( AffineMap ( 0 , 0 ))) by FUNCT_2:def 1;

        

         O4: a < +infty & c < +infty by XXREAL_0: 9, XREAL_0:def 1;

        

         O3: a < c by Z1, Z2, XXREAL_0: 2;

        

         O5: -infty < a by XXREAL_0: 12, XREAL_0:def 1;

         [.a, b.] c= REAL ;

        then

         O1: [.a, b.] c= ( dom ( AffineMap ((1 / (b - a)),( - (a / (b - a)))))) by FUNCT_2:def 1;

         [.b, c.] c= REAL ;

        then

         O2: [.b, c.] c= ( dom ( AffineMap (( - (1 / (c - b))),(c / (c - b))))) by FUNCT_2:def 1;

        (( dom f2) \/ ( dom f3)) = ( [.a, b.] \/ ( dom f3)) by RELAT_1: 62, O1

        .= ( [.a, b.] \/ [.b, c.]) by RELAT_1: 62, O2

        .= [.a, c.] by XXREAL_1: 165, Z1, Z2;

        

        then (( dom f1) \/ (( dom f2) \/ ( dom f3))) = (( REAL \ ].a, c.[) \/ [.a, c.]) by i7, RELAT_1: 62

        .= (( ]. -infty , a.] \/ [.c, +infty .[) \/ [.a, c.]) by XXREAL_1: 398

        .= ( ]. -infty , a.] \/ ( [.c, +infty .[ \/ [.a, c.])) by XBOOLE_1: 4

        .= ( ]. -infty , a.] \/ [.a, +infty .[) by XXREAL_1: 176, O3, O4

        .= ]. -infty , +infty .[ by XXREAL_1: 172, O4, O5;

        then ((( dom f1) \/ ( dom f2)) \/ ( dom f3)) = REAL by XBOOLE_1: 4, XXREAL_1: 224;

        hence thesis by FUNCT_2: 2, I5, I3;

      end;

    end

    theorem :: FUZNUM_1:29

    for a,b,c be Real st a < b & b < c holds ( TriangularFS (a,b,c)) is strictly-normalized

    proof

      let a,b,c be Real;

      set F = ( TriangularFS (a,b,c));

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

      assume

       Z1: a < b & b < c;

      

       s0: bb in [.b, c.] by Z1;

      

       S1: F = (((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) +* (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) by Z1, TrDef;

      

       s2: ( dom ( AffineMap (( - (1 / (c - b))),(c / (c - b))))) = REAL by FUNCT_2:def 1;

      (a + 0 ) < b by Z1;

      then

       T1: (b - a) > 0 by XREAL_1: 20;

      (b + 0 ) < c by Z1;

      then

       t1: (c - b) > 0 by XREAL_1: 20;

      bb in [.b, c.] by Z1;

      then bb in ( dom (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) by s2, RELAT_1: 57;

      

      then

       A1: (F . bb) = ((( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.]) . bb) by FUNCT_4: 13, S1

      .= (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . bb) by FUNCT_1: 49, s0

      .= 1 by Cb1, t1;

      for y be Element of REAL st (F . y) = 1 holds y = bb

      proof

        let y be Element of REAL ;

        assume

         X0: (F . y) = 1;

        per cases ;

          suppose

           X1: y in [.a, b.];

          per cases by XXREAL_1: 7;

            suppose

             x1: y in [.a, b.[;

            y in REAL ;

            then

             X3: y in ( dom ( AffineMap ((1 / (b - a)),( - (a / (b - a)))))) by FUNCT_2:def 1;

            

             X2: y in ( dom (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) by X3, X1, RELAT_1: 57;

             not y in [.b, c.] by x1, XBOOLE_0: 3, XXREAL_1: 95;

            then not y in ( dom (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) by RELAT_1: 57;

            

            then (F . y) = (((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) . y) by FUNCT_4: 11, S1

            .= ((( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.]) . y) by FUNCT_4: 13, X2;

            then (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) . y) = 1 by X1, FUNCT_1: 49, X0;

            hence thesis by Hope3, T1;

          end;

            suppose y = b;

            hence thesis;

          end;

        end;

          suppose

           X1: y in [.b, c.];

          y in REAL ;

          then y in ( dom ( AffineMap (( - (1 / (c - b))),(c / (c - b))))) by FUNCT_2:def 1;

          then y in ( dom (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) by X1, RELAT_1: 57;

          then (F . y) = ((( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.]) . y) by FUNCT_4: 13, S1;

          then (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) . y) = 1 by X1, FUNCT_1: 49, X0;

          hence thesis by Hope4, t1;

        end;

          suppose

           so: not (y in [.a, b.] or y in [.b, c.]);

          then

           s1: not y in ( dom (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) & not y in ( dom (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) by RELAT_1: 57;

          

           s8: ].a, c.[ c= [.a, c.] by XXREAL_1: 25;

           not y in ( [.a, b.] \/ [.b, c.]) by so, XBOOLE_0:def 3;

          then not y in [.a, c.] by XXREAL_1: 165, Z1;

          then

           s7: not y in ].a, c.[ by s8;

          

           ss: y in ( REAL \ ].a, c.[) by s7, XBOOLE_0:def 5;

          (F . y) = (((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) . y) by FUNCT_4: 11, s1, S1

          .= ((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)) . y) by FUNCT_4: 11, s1

          .= (( AffineMap ( 0 , 0 )) . y) by FUNCT_1: 49, ss;

          hence thesis by Hope5, X0;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: FUZNUM_1:30

    for a,b,c be Real st a < b & b < c holds ( TriangularFS (a,b,c)) is continuous

    proof

      let a,b,c be Real;

      assume that

       Z1: a < b and

       Z2: b < c;

      set F = ( TriangularFS (a,b,c));

      

       S1: F = (((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, c.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) +* (( AffineMap (( - (1 / (c - b))),(c / (c - b)))) | [.b, c.])) by Z1, Z2, TrDef;

      set f1 = ( AffineMap ( 0 , 0 ));

      set f = (f1 | ( REAL \ ].a, c.[));

      set g1 = ( AffineMap ((1 / (b - a)),( - (a / (b - a)))));

      reconsider g = (g1 | [.a, b.]) as PartFunc of REAL , REAL ;

      set h1 = ( AffineMap (( - (1 / (c - b))),(c / (c - b))));

      reconsider h = (h1 | [.b, c.]) as PartFunc of REAL , REAL ;

       [.a, b.] c= REAL ;

      then [.a, b.] c= ( dom g1) by FUNCT_2:def 1;

      then

       J2: ( dom g) = [.a, b.] by RELAT_1: 62;

       [.b, c.] c= REAL ;

      then

       h1: [.b, c.] c= ( dom h1) by FUNCT_2:def 1;

      then

       J3: ( dom h) = [.b, c.] by RELAT_1: 62;

      b in ( dom g) by J2, Z1;

      then

       j2: g is non empty;

      b in ( dom h) by J3, Z2;

      then

       j3: h is non empty;

      

       ff: for x be object st x in (( dom g) /\ ( dom h)) holds (g . x) = (h . x)

      proof

        let x be object;

        assume x in (( dom g) /\ ( dom h));

        then

         i1: x in {b} by XXREAL_1: 418, Z1, Z2, J2, J3;

        

         II: b in [.a, b.] & b in [.b, c.] by Z1, Z2;

        (a + 0 ) < b by Z1;

        then

         I0: (b - a) > 0 by XREAL_1: 20;

        (b + 0 ) < c by Z2;

        then

         I2: (c - b) > 0 by XREAL_1: 20;

        (h . x) = (h . b) by i1, TARSKI:def 1

        .= (h1 . b) by FUNCT_1: 49, II

        .= 1 by Cb1, I2

        .= (g1 . b) by I0, Ab1

        .= (g . b) by FUNCT_1: 49, II

        .= (g . x) by i1, TARSKI:def 1;

        hence thesis;

      end;

      then

       fF: g tolerates h by PARTFUN1:def 4;

      set gh = (g +* h);

      

       z1: ( dom gh) = (( dom g) \/ ( dom h)) by FUNCT_4:def 1

      .= ( [.a, b.] \/ [.b, c.]) by J2, h1, RELAT_1: 62

      .= [.a, c.] by XXREAL_1: 165, Z1, Z2;

      

       K2: a in [.a, b.] by Z1;

      

      then

       W3: (gh . a) = (g . a) by FUNCT_4: 15, PARTFUN1:def 4, ff, J2

      .= (g1 . a) by FUNCT_1: 49, K2

      .= 0 by Ah1;

      

       K1: c in [.b, c.] by Z2;

      c in ( dom h) by J3, Z2;

      

      then (gh . c) = (h . c) by FUNCT_4: 13

      .= (h1 . c) by K1, FUNCT_1: 49

      .= 0 by Cb2;

      then

      consider hh be PartFunc of REAL , REAL such that

       TT: hh = (f +* gh) & for x be Real st x in ( dom hh) holds hh is_continuous_in x by W3, Kluczyk, fF, z1, Glue, J2, j2, j3, J3;

      hh = F by TT, FUNCT_4: 14, S1;

      hence thesis by TT;

    end;

    definition

      let a,b,c,d be Real;

      assume that

       Z1: a < b and

       Z2: b < c and

       Z3: c < d;

      :: FUZNUM_1:def8

      func TrapezoidalFS (a,b,c,d) -> FuzzySet of REAL equals

      : TPDef: ((((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, d.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) +* (( AffineMap ( 0 ,1)) | [.b, c.])) +* (( AffineMap (( - (1 / (d - c))),(d / (d - c)))) | [.c, d.]));

      coherence

      proof

        

         k1: (a + 0 ) < b by Z1;

        

         k3: b < d by Z2, Z3, XXREAL_0: 2;

        set f1 = (( AffineMap ( 0 , 0 )) | ( REAL \ ].a, d.[)), f2 = (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.]), f3 = (( AffineMap ( 0 ,1)) | [.b, c.]), f4 = (( AffineMap (( - (1 / (d - c))),(d / (d - c)))) | [.c, d.]);

        set f = (((f1 +* f2) +* f3) +* f4);

        a < c by Z1, Z2, XXREAL_0: 2;

        then ( REAL \ ].a, d.[) <> {} by RealNon, Z3, XXREAL_0: 2;

        then

         L1: ( rng f1) = { 0 } by Andr1a;

        

         L2: ( rng f2) = [. 0 , 1.] by k1, Hope1, XREAL_1: 20;

        b in [.b, c.] by Z2;

        then

         L3: ( rng f3) = {1} by Andr1a;

        (c + 0 ) < d by Z3;

        then

         L4: ( rng f4) = [. 0 , 1.] by Hope2a, XREAL_1: 20;

        

         Ss: ( rng (f1 +* f2)) c= (( rng f1) \/ ( rng f2)) by FUNCT_4: 17;

        ( rng ((f1 +* f2) +* f3)) c= (( rng (f1 +* f2)) \/ ( rng f3)) by FUNCT_4: 17;

        then

         d6: (( rng ((f1 +* f2) +* f3)) \/ ( rng f4)) c= ((( rng (f1 +* f2)) \/ ( rng f3)) \/ ( rng f4)) by XBOOLE_1: 13;

        ( rng f) c= (( rng ((f1 +* f2) +* f3)) \/ ( rng f4)) by FUNCT_4: 17;

        then

         l6: ( rng f) c= ((( rng (f1 +* f2)) \/ ( rng f3)) \/ ( rng f4)) by d6;

         [. 0 , 0 .] c= [. 0 , 1.] by XXREAL_1: 34;

        then

         Hh: { 0 } c= [. 0 , 1.] by XXREAL_1: 17;

         [.1, 1.] c= [. 0 , 1.] by XXREAL_1: 34;

        then {1} c= [. 0 , 1.] by XXREAL_1: 17;

        then

         hx: ( {1} \/ [. 0 , 1.]) = [. 0 , 1.] by XBOOLE_1: 12;

        

         ss: ( rng (f1 +* f2)) c= [. 0 , 1.] by Hh, Ss, L1, L2, XBOOLE_1: 12;

        

         sk: ( rng f) c= (( rng (f1 +* f2)) \/ [. 0 , 1.]) by hx, L3, XBOOLE_1: 4, L4, l6;

        (( rng (f1 +* f2)) \/ [. 0 , 1.]) c= ( [. 0 , 1.] \/ [. 0 , 1.]) by ss, XBOOLE_1: 13;

        then

         I3: ( rng f) c= [. 0 , 1.] by sk;

        

         I5: ( dom f) = (( dom ((f1 +* f2) +* f3)) \/ ( dom f4)) by FUNCT_4:def 1

        .= ((( dom (f1 +* f2)) \/ ( dom f3)) \/ ( dom f4)) by FUNCT_4:def 1

        .= (((( dom f1) \/ ( dom f2)) \/ ( dom f3)) \/ ( dom f4)) by FUNCT_4:def 1;

        ( REAL \ ].a, d.[) c= REAL ;

        then

         i7: ( REAL \ ].a, d.[) c= ( dom ( AffineMap ( 0 , 0 ))) by FUNCT_2:def 1;

        

         O4: a < +infty & c < +infty & d < +infty by XXREAL_0: 9, XREAL_0:def 1;

        a < c by Z1, Z2, XXREAL_0: 2;

        then

         O6: a < d by Z3, XXREAL_0: 2;

        

         O5: -infty < a by XXREAL_0: 12, XREAL_0:def 1;

         [.a, b.] c= REAL ;

        then

         O1: [.a, b.] c= ( dom ( AffineMap ((1 / (b - a)),( - (a / (b - a)))))) by FUNCT_2:def 1;

         [.b, c.] c= REAL ;

        then

         j1: [.b, c.] c= ( dom ( AffineMap ( 0 ,1))) by FUNCT_2:def 1;

         [.c, d.] c= REAL ;

        then

         OO: [.c, d.] c= ( dom ( AffineMap (( - (1 / (d - c))),(d / (d - c))))) by FUNCT_2:def 1;

        

         d2: (( dom f3) \/ ( dom f4)) = ( [.b, c.] \/ ( dom f4)) by j1, RELAT_1: 62

        .= ( [.b, c.] \/ [.c, d.]) by RELAT_1: 62, OO

        .= [.b, d.] by XXREAL_1: 165, Z2, Z3;

        

         d3: ((( dom f2) \/ ( dom f3)) \/ ( dom f4)) = (( dom f2) \/ (( dom f3) \/ ( dom f4))) by XBOOLE_1: 4

        .= ( [.a, b.] \/ [.b, d.]) by d2, O1, RELAT_1: 62

        .= [.a, d.] by XXREAL_1: 165, k3, Z1;

        ((( dom f1) \/ (( dom f2) \/ ( dom f3))) \/ ( dom f4)) = (( dom f1) \/ ((( dom f2) \/ ( dom f3)) \/ ( dom f4))) by XBOOLE_1: 4

        .= (( REAL \ ].a, d.[) \/ [.a, d.]) by d3, i7, RELAT_1: 62

        .= (( ]. -infty , a.] \/ [.d, +infty .[) \/ [.a, d.]) by XXREAL_1: 398

        .= ( ]. -infty , a.] \/ ( [.d, +infty .[ \/ [.a, d.])) by XBOOLE_1: 4

        .= ( ]. -infty , a.] \/ [.a, +infty .[) by XXREAL_1: 176, O4, O6

        .= ]. -infty , +infty .[ by XXREAL_1: 172, O4, O5;

        then (((( dom f1) \/ ( dom f2)) \/ ( dom f3)) \/ ( dom f4)) = REAL by XBOOLE_1: 4, XXREAL_1: 224;

        hence thesis by FUNCT_2: 2, I5, I3;

      end;

    end

    theorem :: FUZNUM_1:31

    for a,b,c,d be Real st a < b & b < c & c < d holds ( TrapezoidalFS (a,b,c,d)) is normalized

    proof

      let a,b,c,d be Real;

      set F = ( TrapezoidalFS (a,b,c,d));

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

      assume

       Z1: a < b & b < c & c < d;

      

       s0: bb in [.c, d.] by Z1;

      

       S1: F = ((((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, d.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) +* (( AffineMap ( 0 ,1)) | [.b, c.])) +* (( AffineMap (( - (1 / (d - c))),(d / (d - c)))) | [.c, d.])) by Z1, TPDef;

      

       s2: ( dom ( AffineMap (( - (1 / (d - c))),(d / (d - c))))) = REAL by FUNCT_2:def 1;

      (c + 0 ) < d by Z1;

      then

       t1: (d - c) > 0 by XREAL_1: 20;

      bb in [.c, d.] by Z1;

      then bb in ( dom (( AffineMap (( - (1 / (d - c))),(d / (d - c)))) | [.c, d.])) by s2, RELAT_1: 57;

      

      then (F . bb) = ((( AffineMap (( - (1 / (d - c))),(d / (d - c)))) | [.c, d.]) . bb) by FUNCT_4: 13, S1

      .= (( AffineMap (( - (1 / (d - c))),(d / (d - c)))) . bb) by FUNCT_1: 49, s0

      .= 1 by Cb1, t1;

      hence thesis;

    end;

    theorem :: FUZNUM_1:32

    for a,b,c,d be Real st a < b & b < c & c < d holds ( TrapezoidalFS (a,b,c,d)) is continuous

    proof

      let a,b,c,d be Real;

      assume that

       Z1: a < b and

       Z2: b < c and

       Z3: c < d;

      set F = ( TrapezoidalFS (a,b,c,d));

      

       S1: F = ((((( AffineMap ( 0 , 0 )) | ( REAL \ ].a, d.[)) +* (( AffineMap ((1 / (b - a)),( - (a / (b - a))))) | [.a, b.])) +* (( AffineMap ( 0 ,1)) | [.b, c.])) +* (( AffineMap (( - (1 / (d - c))),(d / (d - c)))) | [.c, d.])) by Z1, Z2, Z3, TPDef;

      set f1 = ( AffineMap ( 0 , 0 ));

      set f = (f1 | ( REAL \ ].a, d.[));

      set g1 = ( AffineMap ((1 / (b - a)),( - (a / (b - a)))));

      reconsider g = (g1 | [.a, b.]) as PartFunc of REAL , REAL ;

      set h1 = ( AffineMap (( - (1 / (d - c))),(d / (d - c))));

      reconsider h = (h1 | [.c, d.]) as PartFunc of REAL , REAL ;

      set i1 = ( AffineMap ( 0 ,1));

      reconsider i = (i1 | [.b, c.]) as PartFunc of REAL , REAL ;

       [.a, b.] c= REAL ;

      then

       d9: [.a, b.] c= ( dom g1) by FUNCT_2:def 1;

      then

       J2: ( dom g) = [.a, b.] by RELAT_1: 62;

       [.c, d.] c= REAL ;

      then

       d3: [.c, d.] c= ( dom h1) by FUNCT_2:def 1;

      then

       J3: ( dom h) = [.c, d.] by RELAT_1: 62;

       [.b, c.] c= REAL ;

      then

       d8: [.b, c.] c= ( dom i1) by FUNCT_2:def 1;

      then

       JW: ( dom i) = [.b, c.] by RELAT_1: 62;

      b in ( dom g) by J2, Z1;

      then

       j2: g is non empty;

      c in ( dom h) by J3, Z3;

      then

       j3: h is non empty;

      

       ff: for x be object st x in (( dom g) /\ ( dom i)) holds (g . x) = (i . x)

      proof

        let x be object;

        assume x in (( dom g) /\ ( dom i));

        then

         i1: x in {b} by XXREAL_1: 418, Z1, Z2, J2, JW;

        

         II: b in [.a, b.] & b in [.b, c.] by Z1, Z2;

        (a + 0 ) < b by Z1;

        then

         I0: (b - a) > 0 by XREAL_1: 20;

        (i . x) = (i . b) by i1, TARSKI:def 1

        .= (i1 . b) by FUNCT_1: 49, II

        .= 1 by Kici1

        .= (g1 . b) by I0, Ab1

        .= (g . b) by FUNCT_1: 49, II

        .= (g . x) by i1, TARSKI:def 1;

        hence thesis;

      end;

      set gh = (g +* i);

      

       z1: ( dom gh) = (( dom g) \/ ( dom i)) by FUNCT_4:def 1

      .= ( [.a, b.] \/ [.b, c.]) by d9, RELAT_1: 62, JW

      .= [.a, c.] by XXREAL_1: 165, Z1, Z2;

      

       V5: a < c by XXREAL_0: 2, Z1, Z2;

      then

       PS: a in ( dom gh) by z1;

      then

      reconsider gh as non empty PartFunc of REAL , REAL ;

      

       K2: a in [.a, b.] by Z1;

      

      then

       W3: (gh . a) = (g . a) by FUNCT_4: 15, PARTFUN1:def 4, ff, J2

      .= (g1 . a) by FUNCT_1: 49, K2

      .= 0 by Ah1;

      

       P3: c in [.b, c.] by Z2;

      

       K1: c in [.c, d.] by Z3;

      

       N3: ( dom h) = [.c, d.] by d3, RELAT_1: 62;

      (c + 0 ) < d by Z3;

      then

       MN: (d - c) > 0 by XREAL_1: 20;

      

       N4: (h . c) = (h1 . c) by FUNCT_1: 49, K1

      .= 1 by Cb1, MN;

      

       KK: d in [.c, d.] by Z3;

      

      then

       N5: (h . d) = (h1 . d) by FUNCT_1: 49

      .= 0 by Cb2;

      

       NN: gh is continuous by Glue, ff, j2, J2, JW, d8, P3, PARTFUN1:def 4;

      

       M1: for x be object st x in (( dom gh) /\ ( dom h)) holds (gh . x) = (h . x)

      proof

        let x be object;

        assume x in (( dom gh) /\ ( dom h));

        then

         ll: x in {c} by XXREAL_1: 418, Z3, V5, J3, z1;

        

        then (gh . x) = (gh . c) by TARSKI:def 1

        .= (i . c) by FUNCT_4: 13, P3, JW

        .= (i1 . c) by FUNCT_1: 49, P3

        .= (h . c) by N4, Kici1

        .= (h . x) by ll, TARSKI:def 1;

        hence thesis;

      end;

      then

       fG: gh tolerates h by PARTFUN1:def 4;

      set ghi = (gh +* h);

      

       V3: ( dom ghi) = (( dom gh) \/ ( dom h)) by FUNCT_4:def 1

      .= ( [.a, c.] \/ [.c, d.]) by z1, d3, RELAT_1: 62

      .= [.a, d.] by XXREAL_1: 165, Z3, V5;

      

       V4: (ghi . a) = 0 by FUNCT_4: 15, M1, PARTFUN1:def 4, PS, W3;

      (ghi . d) = 0 by N3, FUNCT_4: 13, KK, N5;

      then

      consider hh be PartFunc of REAL , REAL such that

       TT: hh = (f +* ghi) & for x be Real st x in ( dom hh) holds hh is_continuous_in x by Kluczyk, V3, V4, Glue, NN, j3, z1, J3, fG;

      hh = ((f +* (g +* i)) +* h) by FUNCT_4: 14, TT

      .= (((f +* g) +* i) +* h) by FUNCT_4: 14;

      hence thesis by TT, S1;

    end;

    definition

      let F be FuzzySet of REAL ;

      :: FUZNUM_1:def9

      attr F is triangular means ex a,b,c be Real st F = ( TriangularFS (a,b,c));

      :: FUZNUM_1:def10

      attr F is trapezoidal means ex a,b,c,d be Real st F = ( TrapezoidalFS (a,b,c,d));

    end

    registration

      cluster triangular for FuzzySet of REAL ;

      existence

      proof

        take ( TriangularFS ( 0 ,1,2));

        thus thesis;

      end;

      cluster trapezoidal for FuzzySet of REAL ;

      existence

      proof

        take ( TrapezoidalFS ( 0 ,1,2,3));

        thus thesis;

      end;

    end