:: The Formal Construction of Fuzzy Numbers
::  by Adam Grabowski
:: 
:: Received December 31, 2014
:: Copyright (c) 2014-2016 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, TARSKI,
      FUNCT_1, XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1,
      GRAPH_2, MEASURE5, MSALIMIT, FUZNUM_1, REAL_1, ORDINAL2, XXREAL_2,
      TREES_1, RCOMP_1, ZFMISC_1, NUMPOLY1, JGRAPH_2, FUNCT_4, PRE_TOPC,
      FCONT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XXREAL_2,
      COMPLEX1, XREAL_0, FUNCT_1, PARTFUN1, FCONT_1, RELSET_1, FUNCT_4,
      RCOMP_1, MEASURE5, FUZZY_1;
 constructors COMPLEX1, RFUNCT_1, INTEGRA1, SEQ_4, RELSET_1, FUZZY_1, FCONT_1,
      FUNCT_4;
 registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
      FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, RELAT_1, TOPREALB, FUNCT_4, FUNCT_1,
      XCMPLX_0, NAT_1, RCOMP_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, TARSKI, XXREAL_2;
 equalities FUZZY_1, RCOMP_1;
 expansions TARSKI, FCONT_1;
 theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, ZFMISC_1, XBOOLE_0,
      XBOOLE_1, COMPLEX1, XREAL_1, XXREAL_0, XXREAL_1, FUNCT_2, RELAT_1,
      MEASURE5, XREAL_0, XXREAL_2, FCONT_1, XCMPLX_1, FUZZY_2, FUNCT_4,
      RCOMP_1, ENUMSET1;

begin :: Preliminaries: Affine Maps

theorem RealNon:
  for a,b being Real st a <= b holds
    REAL \ ].a,b.[ <> {}
  proof
    let a,b be Real;
    assume a <= b;
    consider c being 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 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 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 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 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 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 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
  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 being 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 Andr1a:
  for C being 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 being 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 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 being 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
  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 being 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 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 being 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 Hope5:
  (AffineMap (0,0)).x <> 1
  proof
    (AffineMap (0,0)).x = 0 * x + 0 by FCONT_1:def 4 .= 0;
    hence thesis;
  end;

theorem
  AffineMap (0,1).b = 1
  proof
    AffineMap (0,1).b = 0*b + 1 by FCONT_1:def 4 .= 1;
    hence thesis;
  end;

theorem Kici1:
  for a being 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 :: Towards Development of Fuzzy Numbers

 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;
  attr F is normalized means
    ex x being 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;
  attr F is strictly-normalized means
    ex x being Element of C st
      F.x = 1 &
      for y being 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;
  func alpha-cut F -> Subset of C equals
    { x where x is Element of C : F.x >= alpha };
  coherence
  proof
    set H = { x where x is Element of C : F.x >= alpha };
    H c= C
    proof
      let y be object;
      assume y in H; then
      consider x being Element of C such that
A1:   y = x & F.x >= alpha;
      thus thesis by A1;
    end;
    hence thesis;
  end;
end;

theorem AlphaCut1:
  for F being FuzzySet of C,
      alpha being 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 being 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 being 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;
  func Core F -> Subset of C equals
    { x where x is Element of C : F.x = 1 };
  coherence
  proof
    set H = { x where x is Element of C : F.x = 1 };
    H c= C
    proof
      let y be object;
      assume y in H; then
      consider x being Element of C such that
A1:   y = x & F.x = 1;
      thus thesis by A1;
    end;
    hence thesis;
  end;
end;

theorem
  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 CEmpty:
  Core EMF C = {}
  proof
    thus Core EMF C c= {}
    proof
      let x be object;
      assume x in Core EMF C; then
      consider xx being 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 CCounter:
  for F being 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 being 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
  for F being 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 :: Convexity and the Height of a Fuzzy Set

definition let F be FuzzySet of REAL;
  attr F is f-convex means
    for x1, x2 being Real,
        l being 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 being Real,
        l being 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 being Real,
        l being 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;
  func height F -> ExtReal equals
    sup rng F;
  coherence;
end;

theorem HgtBnd:
  for F being 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 being 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 being 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
  for F being 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 being 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 :: Pasting aka Glueing Lemmas

theorem
  for f,g being PartFunc of REAL, REAL st
  f is continuous & g is continuous &
  ex x being object st dom f /\ dom g = {x} &
  for x being object st x in dom f /\ dom g holds f.x = g.x holds
    ex h being PartFunc of REAL, REAL st
    h = f +* g & for x being 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 being object st dom f /\ dom g = {x} &
    for x being 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 by FUNCT_4:23;
j2: h | dom g = g by FUNCT_4:23;
    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 being Real st 0 < r
     ex s being Real st 0 < s &
    for x1 being 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 RELAT_1:57,JJ,ZR;
      assume
R0:   0 < r;
      consider s2 being Real such that
SB:   0 < s2 & for x1 being 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 being Real such that
Sb:   0 < s1 & for x1 being Real st x1 in dom hg & |.x1-x.| < s1 holds
        |.hg.x1 - hg.x.| < r / 2 by FCONT_1:3,j2,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; then
        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; then
p1:       x1 in dom h by FUNCT_4:12; then
          x1 in dom hg by RELAT_1:57,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,RELAT_1:57,P1;
          hence thesis by SS,XXREAL_0:2,P3,P2;
      end;
    end;
    hence thesis by FCONT_1:3;
  end;

theorem LemGlue:
  for f,g being PartFunc of REAL, REAL st
  f is continuous non empty & g is continuous non empty &
  (ex a,b,c being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
  f tolerates g
    ex h being PartFunc of REAL, REAL st
    h = f +* g & for x being 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 being 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 being 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 by FUNCT_4:23;
j2: h | dom g = g by FUNCT_4:23;
    assume
JJ: x in dom h; then
    per cases by FUNCT_4:12;
    suppose
J1: x in dom f;
    set hf = h |dom f;
    set hg = h |dom g;
    for r being Real st 0 < r
     ex s being Real st 0 < s &
    for x1 being 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 being Real such that
SB:   0 < s2 & for x1 being 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 being Real such that
Sb:   0 < s1 & for x1 being Real st x1 in dom hg & |.x1-b.|<s1 holds
        |.hg.x1-hg.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 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 by RELAT_1:57,SC; 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,j2,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,RELAT_1:57,SC;
          |.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 being Real st 0<r ex s being Real st 0<s &
    for x1 being 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 RELAT_1:57,J1,JJ;
      assume
R0:   0 < r; then
      consider s2 being Real such that
SB:   0 < s2 & for x1 being Real st x1 in dom hg & |.x1-x.|<s2 holds
        |.hg.x1-hg.x.| < r/2 by J1,FCONT_1:3,j2,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 being Real such that
Sb:   0 < s1 & for x1 being 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 by RELAT_1:57,SC;
SD:       |.hg.x1 - hg.x.| < r / 2 by SB,ZT,H1,RELAT_1:57,SC;
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,j2,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 Glue:
  for f,g being PartFunc of REAL, REAL st
    f is continuous non empty &
    g is continuous non empty &
    (ex a,b,c being 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 being Real st dom f = [.a,b.] & dom g = [.b,c.]) &
      f tolerates g; then
    consider h being PartFunc of REAL, REAL such that
A2: h = f +* g & for x being Real st x in dom h holds h is_continuous_in x
      by LemGlue;
    thus thesis by A2;
  end;

theorem Asi1:
  for f, g being 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 being 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 Kluczyk:
  for f, g being 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 being PartFunc of REAL, REAL st h = f +* g &
  for x being 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; then
    per cases by TARSKI:def 2;
    suppose
FT:   x = a;
      for r being Real st 0 < r
       ex s being Real st 0 < s &
      for x1 being 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 being Real such that
WW:     0 < s1 &
        for x1 being Real st x1 in dom g & |.x1-x.|<s1 holds |.g.x1-g.x.| < r
          by FCONT_1:3,A1,sx,FT;
        consider s2 being Real such that
W1:     0 < s2 &
        for x1 being 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; then
        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 being Real st 0<r
       ex s being Real st 0<s &
      for x1 being 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 being Real such that
WW:     0 < s1 &
        for x1 being Real st x1 in dom g & |.x1-x.|<s1 holds |.g.x1-g.x.| < r
          by FCONT_1:3,A1,sy,FT;
        consider s2 being Real such that
W1:     0 < s2 &
        for x1 being 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; then
        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 being Neighbourhood of h.xx0
     ex N being Neighbourhood of xx0 st
     for x1 being 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 being Neighbourhood of xx0 such that
D0:    for x1 being 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 being 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 being Neighbourhood of h.xx0
        ex N being Neighbourhood of xx0 st
        for x1 being 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 being Neighbourhood of xx0 such that
  D0:     for x1 being 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 being 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 being Neighbourhood of h.xx0
        ex N being Neighbourhood of xx0 st
        for x1 being 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 being Neighbourhood of xx0 such that
  D0:     for x1 being 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 being 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
  for f, g being 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 being PartFunc of REAL, REAL such that
A2: h = f +* g &
    for x being 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 :: Triangular and Trapezoidal Fuzzy Sets

definition let a,b,c be Real;
  assume that
Z1:  a < b and
Z2:  b < c;
  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;

::definition let C; let a,b,c be Real;
::  func TriangularFS (C,a,b,c) -> FuzzySet of C means
::    for x being Real st x in C holds
::    ((x <= a or c <= x) implies it.x = 0) &
::    (a <= x & x <= b implies it.x = (x-a)/(b-a)) &
::    (b <= x & x <= c implies it.x = (c-x)/(c-b));
::  correctness;
::end;

theorem
  for a,b,c being 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 being 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.]; then
        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
  for a,b,c being 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 being 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 being PartFunc of REAL, REAL such that
TT: hh = f +* gh &
    for x being 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;
  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
  for a,b,c,d being 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
  for a,b,c,d being 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 being 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 being 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 being PartFunc of REAL, REAL such that
TT: hh = f +* ghi &
    for x being 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;
  attr F is triangular means
    ex a,b,c being Real st F = TriangularFS (a,b,c);
  attr F is trapezoidal means
    ex a,b,c,d being 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;