:: FUZZY_4 semantic presentation

begin


registration
let C1 be non empty set ;
let F be Membership_Func of C1;
cluster rng F ->  non empty ;
coherence
 not rng F is empty
proof
 dom F = C1 by FUNCT_2:def_1;
then consider y being Element of C1 such that
A1: y in dom F by SUBSET_1:4;
 F . y in rng F by A1, FUNCT_1:def_3;
hence  not rng F is empty ; ::_thesis: verum
end;
end;

theorem Th1: :: FUZZY_4:1
for C1 being non empty set
for F being Membership_Func of C1 holds
( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) )
proof
let C1 be non empty set ; ::_thesis: for F being Membership_Func of C1 holds
( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) )
let F be Membership_Func of C1; ::_thesis: ( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) )
A1: [.0,1.] is non empty closed_interval Subset of REAL by MEASURE5:14;
A2: rng F c= [.0,1.] by RELAT_1:def_19;
then A3: rng F is real-bounded by A1, XXREAL_2:45;
A4: for x being set st x in dom F holds
F . x >= lower_bound (rng F)
proof
let x be set ; ::_thesis: ( x in dom F implies F . x >= lower_bound (rng F) )
assume  x in dom F ; ::_thesis: F . x >= lower_bound (rng F)
then A5: F . x in rng F by FUNCT_1:def_3;
 rng F is bounded_below by A3, XXREAL_2:def_11;
hence  F . x >= lower_bound (rng F) by A5, SEQ_4:def_2; ::_thesis: verum
end;
 for x being set st x in dom F holds
F . x <= upper_bound (rng F)
proof
let x be set ; ::_thesis: ( x in dom F implies F . x <= upper_bound (rng F) )
assume  x in dom F ; ::_thesis: F . x <= upper_bound (rng F)
then A6: F . x in rng F by FUNCT_1:def_3;
 rng F is bounded_above by A3, XXREAL_2:def_11;
hence  F . x <= upper_bound (rng F) by A6, SEQ_4:def_1; ::_thesis: verum
end;
hence  ( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) ) by A2, A1, A4, XXREAL_2:45; ::_thesis: verum
end;

theorem :: FUZZY_4:2
for C1 being non empty set
for F, G being Membership_Func of C1 st ( for x being set st x in C1 holds
F . x <= G . x ) holds
upper_bound (rng F) <= upper_bound (rng G)
proof
let C1 be non empty set ; ::_thesis: for F, G being Membership_Func of C1 st ( for x being set st x in C1 holds
F . x <= G . x ) holds
upper_bound (rng F) <= upper_bound (rng G)
let F, G be Membership_Func of C1; ::_thesis: ( ( for x being set st x in C1 holds
F . x <= G . x ) implies upper_bound (rng F) <= upper_bound (rng G) )
 rng F is real-bounded by Th1;
then A1: rng F is bounded_above by XXREAL_2:def_11;
assume A2: for c being set st c in C1 holds
F . c <= G . c ; ::_thesis: upper_bound (rng F) <= upper_bound (rng G)
A3: for s being real number st 0 < s holds
ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y )
then consider r being real number  such that
A4: r in rng F and
A5: (upper_bound (rng F)) - s < r by A1, SEQ_4:def_1;
consider y being set  such that
A6: y in dom F and
A7: r = F . y by A4, FUNCT_1:def_3;
 r <= G . y by A2, A6, A7;
hence  ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y ) by A5, A6, XXREAL_0:2; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng F)) - s <= upper_bound (rng G)
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng F)) - s <= upper_bound (rng G) )
assume  0 < s ; ::_thesis: (upper_bound (rng F)) - s <= upper_bound (rng G)
then consider y being set  such that
A8: y in dom F and
A9: (upper_bound (rng F)) - s <= G . y by A3;
 y in C1 by A8;
then  y in dom G by FUNCT_2:def_1;
then  G . y <= upper_bound (rng G) by Th1;
hence  (upper_bound (rng F)) - s <= upper_bound (rng G) by A9, XXREAL_0:2; ::_thesis: verum
end;
hence  upper_bound (rng F) <= upper_bound (rng G) by XREAL_1:57; ::_thesis: verum
end;

theorem Th3: :: FUZZY_4:3
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2
for c being set holds
( 0 <= f . c & f . c <= 1 )
proof
let C1, C2 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for c being set holds
( 0 <= f . c & f . c <= 1 )
let f be RMembership_Func of C1,C2; ::_thesis: for c being set holds
( 0 <= f . c & f . c <= 1 )
let c be set ; ::_thesis: ( 0 <= f . c & f . c <= 1 )
percases ( c in [:C1,C2:] or not c in [:C1,C2:] ) ;
suppose c in [:C1,C2:] ; ::_thesis: ( 0 <= f . c & f . c <= 1 )
then reconsider c = c as Element of [:C1,C2:] ;
A1: f . c <= (Umf (C1,C2)) . c by FUZZY_2:52;
 (Zmf (C1,C2)) . c <= f . c by FUZZY_2:52;
hence  ( 0 <= f . c & f . c <= 1 ) by A1, FUNCT_3:def_3; ::_thesis: verum
end;
supposeA2: not c in [:C1,C2:] ; ::_thesis: ( 0 <= f . c & f . c <= 1 )
 dom f = [:C1,C2:] by FUNCT_2:def_1;
hence  ( 0 <= f . c & f . c <= 1 ) by A2, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;

definition
let C1, C2 be non empty set ;
let f be RMembership_Func of C1,C2;
let x, y be set ;
:: original: .
redefine funcf . (x,y) ->  Element of REAL ;
coherence
 f . (x,y) is Element of REAL
proof
 f . (x,y) = f . [x,y] ;
hence  f . (x,y) is Element of REAL ; ::_thesis: verum
end;
end;

theorem :: FUZZY_4:4
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2
for x, y being set holds
( 0 <= f . (x,y) & f . (x,y) <= 1 ) by Th3;

begin

notation
let C1, C2 be non empty set ;
let h be RMembership_Func of C2,C1;
synonym  converse h for  ~ C1;
end;

definition
let C1, C2 be non empty set ;
let h be RMembership_Func of C2,C1;
:: original: converse
redefine func converse h ->  RMembership_Func of C1,C2 means :Def1: :: FUZZY_4:def 1
 for x, y being set st [x,y] in [:C1,C2:] holds
it . (x,y) = h . (y,x);
coherence
 converse is RMembership_Func of C1,C2
proof
set IT = converse ;
A1: dom h = [:C2,C1:] by FUNCT_2:def_1;
then A2: dom (converse ) = [:C1,C2:] by FUNCT_4:46;
 rng h c= [.0,1.] by RELAT_1:def_19;
then A3: rng (converse ) c= [.0,1.] by A1, FUNCT_4:47;
then  rng (converse ) c= REAL by MEMBERED:3;
then reconsider IT = converse as PartFunc of [:C1,C2:],REAL by A2, RELSET_1:4;
 IT is Membership_Func of [:C1,C2:] by A2, A3, FUNCT_2:def_1, RELAT_1:def_19;
hence  converse is RMembership_Func of C1,C2 ; ::_thesis: verum
end;
compatibility
 for b1 being RMembership_Func of C1,C2 holds
( b1 = converse iff for x, y being set st [x,y] in [:C1,C2:] holds
b1 . (x,y) = h . (y,x) )
proof
let IT be RMembership_Func of C1,C2; ::_thesis: ( IT = converse iff for x, y being set st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) )
A4: dom h = [:C2,C1:] by FUNCT_2:def_1;
thus  ( IT = ~ h implies for x, y being set st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) ) ::_thesis: ( ( for x, y being set st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) ) implies IT = converse )
proof
assume A5: IT = ~ h ; ::_thesis: for x, y being set st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x)
let x, y be set ; ::_thesis: ( [x,y] in [:C1,C2:] implies IT . (x,y) = h . (y,x) )
assume  [x,y] in [:C1,C2:] ; ::_thesis: IT . (x,y) = h . (y,x)
then  [y,x] in dom h by A4, ZFMISC_1:88;
hence  IT . (x,y) = h . (y,x) by A5, FUNCT_4:def_2; ::_thesis: verum
end;
A6: dom IT = [:C1,C2:] by FUNCT_2:def_1;
A7: for x being set holds
( x in dom IT iff ex y, z being set st
( x = [z,y] & [y,z] in dom h ) )
proof
let x be set ; ::_thesis: ( x in dom IT iff ex y, z being set st
( x = [z,y] & [y,z] in dom h ) )
thus  ( x in dom IT implies ex y, z being set st
( x = [z,y] & [y,z] in dom h ) ) ::_thesis: ( ex y, z being set st
( x = [z,y] & [y,z] in dom h ) implies x in dom IT )
proof
assume  x in dom IT ; ::_thesis: ex y, z being set st
( x = [z,y] & [y,z] in dom h )
then consider z, y being set  such that
A8: z in C1 and
A9: y in C2 and
A10: x = [z,y] by ZFMISC_1:def_2;
take  y ; ::_thesis: ex z being set st
( x = [z,y] & [y,z] in dom h )
take  z ; ::_thesis: ( x = [z,y] & [y,z] in dom h )
thus  ( x = [z,y] & [y,z] in dom h ) by A4, A8, A9, A10, ZFMISC_1:def_2; ::_thesis: verum
end;
thus  ( ex y, z being set st
( x = [z,y] & [y,z] in dom h ) implies x in dom IT ) by A6, ZFMISC_1:88; ::_thesis: verum
end;
assume  for x, y being set st [x,y] in [:C1,C2:] holds
IT . (x,y) = h . (y,x) ; ::_thesis: IT = converse
then  for y, z being set st [y,z] in dom h holds
IT . (z,y) = h . (y,z) by ZFMISC_1:88;
hence  IT = converse by A7, FUNCT_4:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines converse FUZZY_4:def_1_:_
 for C1, C2 being non empty set
for h being RMembership_Func of C2,C1
for b4 being RMembership_Func of C1,C2 holds
( b4 = converse h iff for x, y being set st [x,y] in [:C1,C2:] holds
b4 . (x,y) = h . (y,x) );

theorem :: FUZZY_4:5
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2 holds converse (converse f) = f
proof
let C1, C2 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2 holds converse (converse f) = f
let f be RMembership_Func of C1,C2; ::_thesis: converse (converse f) = f
A1: dom f = [:C1,C2:] by FUNCT_2:def_1;
A2: for c being Element of [:C1,C2:] st c in [:C1,C2:] holds
(converse (converse f)) . c = f . c
proof
let c be Element of [:C1,C2:]; ::_thesis: ( c in [:C1,C2:] implies (converse (converse f)) . c = f . c )
assume  c in [:C1,C2:] ; ::_thesis: (converse (converse f)) . c = f . c
consider x, y being set  such that
A3: x in C1 and
A4: y in C2 and
A5: c = [x,y] by ZFMISC_1:def_2;
A6: [y,x] in [:C2,C1:] by A3, A4, ZFMISC_1:87;
(converse (converse f)) . (x,y) = (converse f) . (y,x) by A5, Def1
.= f . (x,y) by A6, Def1 ;
hence  (converse (converse f)) . c = f . c by A5; ::_thesis: verum
end;
 dom (converse (converse f)) = [:C1,C2:] by FUNCT_2:def_1;
hence  converse (converse f) = f by A2, A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th6: :: FUZZY_4:6
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2 holds 1_minus (converse f) = converse (1_minus f)
proof
let C1, C2 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2 holds 1_minus (converse f) = converse (1_minus f)
let f be RMembership_Func of C1,C2; ::_thesis: 1_minus (converse f) = converse (1_minus f)
A1: [:C2,C1:] = dom (converse (1_minus f)) by FUNCT_2:def_1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds
(1_minus (converse f)) . c = (converse (1_minus f)) . c
proof
let c be Element of [:C2,C1:]; ::_thesis: ( c in [:C2,C1:] implies (1_minus (converse f)) . c = (converse (1_minus f)) . c )
assume  c in [:C2,C1:] ; ::_thesis: (1_minus (converse f)) . c = (converse (1_minus f)) . c
consider y, x being set  such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def_2;
A6: [x,y] in [:C1,C2:] by A3, A4, ZFMISC_1:87;
(1_minus (converse f)) . (y,x) = 1 - ((converse f) . (y,x)) by A5, FUZZY_1:def_5
.= 1 - (f . (x,y)) by A5, Def1
.= (1_minus f) . (x,y) by A6, FUZZY_1:def_5
.= (converse (1_minus f)) . (y,x) by A5, Def1 ;
hence  (1_minus (converse f)) . c = (converse (1_minus f)) . c by A5; ::_thesis: verum
end;
 dom (1_minus (converse f)) = [:C2,C1:] by FUNCT_2:def_1;
hence  1_minus (converse f) = converse (1_minus f) by A2, A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th7: :: FUZZY_4:7
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (max (f,g)) = max ((converse f),(converse g))
proof
let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 holds converse (max (f,g)) = max ((converse f),(converse g))
let f, g be RMembership_Func of C1,C2; ::_thesis: converse (max (f,g)) = max ((converse f),(converse g))
A1: dom (max ((converse f),(converse g))) = [:C2,C1:] by FUNCT_2:def_1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds
(converse (max (f,g))) . c = (max ((converse f),(converse g))) . c
proof
let c be Element of [:C2,C1:]; ::_thesis: ( c in [:C2,C1:] implies (converse (max (f,g))) . c = (max ((converse f),(converse g))) . c )
assume  c in [:C2,C1:] ; ::_thesis: (converse (max (f,g))) . c = (max ((converse f),(converse g))) . c
consider y, x being set  such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def_2;
A6: [x,y] in [:C1,C2:] by A3, A4, ZFMISC_1:87;
(converse (max (f,g))) . (y,x) = (max (f,g)) . (x,y) by A5, Def1
.= max ((f . (x,y)),(g . (x,y))) by A6, FUZZY_1:def_4
.= max (((converse f) . (y,x)),(g . (x,y))) by A5, Def1
.= max (((converse f) . (y,x)),((converse g) . (y,x))) by A5, Def1
.= (max ((converse f),(converse g))) . (y,x) by A5, FUZZY_1:def_4 ;
hence  (converse (max (f,g))) . c = (max ((converse f),(converse g))) . c by A5; ::_thesis: verum
end;
 dom (converse (max (f,g))) = [:C2,C1:] by FUNCT_2:def_1;
hence  converse (max (f,g)) = max ((converse f),(converse g)) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

theorem Th8: :: FUZZY_4:8
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (min (f,g)) = min ((converse f),(converse g))
proof
let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 holds converse (min (f,g)) = min ((converse f),(converse g))
let f, g be RMembership_Func of C1,C2; ::_thesis: converse (min (f,g)) = min ((converse f),(converse g))
A1: dom (min ((converse f),(converse g))) = [:C2,C1:] by FUNCT_2:def_1;
A2: for c being Element of [:C2,C1:] st c in [:C2,C1:] holds
(converse (min (f,g))) . c = (min ((converse f),(converse g))) . c
proof
let c be Element of [:C2,C1:]; ::_thesis: ( c in [:C2,C1:] implies (converse (min (f,g))) . c = (min ((converse f),(converse g))) . c )
assume  c in [:C2,C1:] ; ::_thesis: (converse (min (f,g))) . c = (min ((converse f),(converse g))) . c
consider y, x being set  such that
A3: y in C2 and
A4: x in C1 and
A5: c = [y,x] by ZFMISC_1:def_2;
A6: [x,y] in [:C1,C2:] by A3, A4, ZFMISC_1:87;
(converse (min (f,g))) . (y,x) = (min (f,g)) . (x,y) by A5, Def1
.= min ((f . (x,y)),(g . (x,y))) by A6, FUZZY_1:def_3
.= min (((converse f) . (y,x)),(g . (x,y))) by A5, Def1
.= min (((converse f) . (y,x)),((converse g) . (y,x))) by A5, Def1 ;
hence  (converse (min (f,g))) . c = (min ((converse f),(converse g))) . c by A5, FUZZY_1:def_3; ::_thesis: verum
end;
 dom (converse (min (f,g))) = [:C2,C1:] by FUNCT_2:def_1;
hence  converse (min (f,g)) = min ((converse f),(converse g)) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

theorem Th9: :: FUZZY_4:9
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2
for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds
(converse f) . [y,x] <= (converse g) . [y,x]
proof
let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds
(converse f) . [y,x] <= (converse g) . [y,x]
let f, g be RMembership_Func of C1,C2; ::_thesis: for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds
(converse f) . [y,x] <= (converse g) . [y,x]
let x, y be set ; ::_thesis: ( x in C1 & y in C2 & f . [x,y] <= g . [x,y] implies (converse f) . [y,x] <= (converse g) . [y,x] )
assume that
A1: x in C1 and
A2: y in C2 and
A3: f . [x,y] <= g . [x,y] ; ::_thesis: (converse f) . [y,x] <= (converse g) . [y,x]
A4: [y,x] in [:C2,C1:] by A1, A2, ZFMISC_1:87;
then A5: g . (x,y) = (converse g) . (y,x) by Def1;
 f . (x,y) = (converse f) . (y,x) by A4, Def1;
hence  (converse f) . [y,x] <= (converse g) . [y,x] by A3, A5; ::_thesis: verum
end;

theorem :: FUZZY_4:10
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 st g c= holds
converse g c=
proof
let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 st g c= holds
converse g c=
let f, g be RMembership_Func of C1,C2; ::_thesis: ( g c= implies converse g c= )
assume A1: g c= ; ::_thesis: converse g c=
let c be Element of [:C2,C1:]; :: according to FUZZY_1:def_2 ::_thesis: (converse f) . c <= (converse g) . c
 ex y, x being set st
( y in C2 & x in C1 & c = [y,x] ) by ZFMISC_1:def_2;
then consider x, y being set  such that
A2: x in C1 and
A3: y in C2 and
A4: c = [y,x] ;
 [x,y] in [:C1,C2:] by A2, A3, ZFMISC_1:87;
then  f . [x,y] <= g . [x,y] by A1, FUZZY_1:def_2;
hence  (converse f) . c <= (converse g) . c by A2, A3, A4, Th9; ::_thesis: verum
end;

theorem :: FUZZY_4:11
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (f \ g) = (converse f) \ (converse g)
proof
let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 holds converse (f \ g) = (converse f) \ (converse g)
let f, g be RMembership_Func of C1,C2; ::_thesis: converse (f \ g) = (converse f) \ (converse g)
converse (f \ g) = min ((converse f),(converse (1_minus g))) by Th8
.= min ((converse f),(1_minus (converse g))) by Th6 ;
hence  converse (f \ g) = (converse f) \ (converse g) ; ::_thesis: verum
end;

theorem :: FUZZY_4:12
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (f \+\ g) = (converse f) \+\ (converse g)
proof
let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 holds converse (f \+\ g) = (converse f) \+\ (converse g)
let f, g be RMembership_Func of C1,C2; ::_thesis: converse (f \+\ g) = (converse f) \+\ (converse g)
converse (f \+\ g) = max ((converse (min (f,(1_minus g)))),(converse (min ((1_minus f),g)))) by Th7
.= max ((min ((converse f),(converse (1_minus g)))),(converse (min ((1_minus f),g)))) by Th8
.= max ((min ((converse f),(converse (1_minus g)))),(min ((converse (1_minus f)),(converse g)))) by Th8
.= max ((min ((converse f),(1_minus (converse g)))),(min ((converse (1_minus f)),(converse g)))) by Th6
.= max ((min ((converse f),(1_minus (converse g)))),(min ((1_minus (converse f)),(converse g)))) by Th6 ;
hence  converse (f \+\ g) = (converse f) \+\ (converse g) ; ::_thesis: verum
end;

begin

definition
let C1, C2, C3 be non empty set ;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
let x, z be set ;
assume that
A1: x in C1 and
A2: z in C3 ;
func min (h,g,x,z) ->  Membership_Func of C2 means :Def2: :: FUZZY_4:def 2
 for y being Element of C2 holds it . y = min ((h . [x,y]),(g . [y,z]));
existence
 ex b1 being Membership_Func of C2 st
for y being Element of C2 holds b1 . y = min ((h . [x,y]),(g . [y,z]))
proof
defpred S1[ set , set ] means $2 = min ((h . [x,$1]),(g . [$1,z]));
A3: for y, c1, c2 being set st y in C2 & S1[y,c1] & S1[y,c2] holds
c1 = c2 ;
A4: for y, c being set st y in C2 & S1[y,c] holds
c in REAL ;
consider IT being PartFunc of C2,REAL such that
A5: ( ( for y being set holds
( y in dom IT iff ( y in C2 & ex c being set st S1[y,c] ) ) ) & ( for y being set st y in dom IT holds
S1[y,IT . y] ) ) from PARTFUN1:sch_2(A4, A3);
A6: ( dom IT = C2 & rng IT c= [.0,1.] )
proof
 C2 c= dom IT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in C2 or y in dom IT )
A7: ex c being set st c = min ((h . [x,y]),(g . [y,z])) ;
assume  y in C2 ; ::_thesis: y in dom IT
hence  y in dom IT by A5, A7; ::_thesis: verum
end;
hence  dom IT = C2 by XBOOLE_0:def_10; ::_thesis: rng IT c= [.0,1.]
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in rng IT or c in [.0,1.] )
A8: rng h c= [.0,1.] by RELAT_1:def_19;
assume  c in rng IT ; ::_thesis: c in [.0,1.]
then consider y being Element of C2 such that
A9: y in dom IT and
A10: c = IT . y by PARTFUN1:3;
A11: h . [x,y] >= min ((h . [x,y]),(g . [y,z])) by XXREAL_0:17;
 [x,y] in [:C1,C2:] by A1, ZFMISC_1:87;
then  [x,y] in dom h by FUNCT_2:def_1;
then A12: h . [x,y] in rng h by FUNCT_1:def_3;
 [y,z] in [:C2,C3:] by A2, ZFMISC_1:87;
then  [y,z] in dom g by FUNCT_2:def_1;
then A13: g . [y,z] in rng g by FUNCT_1:def_3;
A14: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A15: 0 = lower_bound A by INTEGRA1:5;
A16: 1 = upper_bound A by A14, INTEGRA1:5;
then  h . [x,y] <= 1 by A8, A12, INTEGRA2:1;
then  min ((h . [x,y]),(g . [y,z])) <= 1 by A11, XXREAL_0:2;
then A17: IT . y <= 1 by A5, A9;
 rng g c= [.0,1.] by RELAT_1:def_19;
then A18: 0 <= g . [y,z] by A15, A13, INTEGRA2:1;
 0 <= h . [x,y] by A8, A15, A12, INTEGRA2:1;
then  0 <= min ((h . [x,y]),(g . [y,z])) by A18, XXREAL_0:20;
then  0 <= IT . y by A5, A9;
hence  c in [.0,1.] by A10, A15, A16, A17, INTEGRA2:1; ::_thesis: verum
end;
then A19: IT is Membership_Func of C2 by FUNCT_2:def_1, RELAT_1:def_19;
 for y being Element of C2 holds IT . y = min ((h . [x,y]),(g . [y,z])) by A5, A6;
hence  ex b1 being Membership_Func of C2 st
for y being Element of C2 holds b1 . y = min ((h . [x,y]),(g . [y,z])) by A19; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Membership_Func of C2 st ( for y being Element of C2 holds b1 . y = min ((h . [x,y]),(g . [y,z])) ) & ( for y being Element of C2 holds b2 . y = min ((h . [x,y]),(g . [y,z])) ) holds
b1 = b2
proof
let F, G be Membership_Func of C2; ::_thesis: ( ( for y being Element of C2 holds F . y = min ((h . [x,y]),(g . [y,z])) ) & ( for y being Element of C2 holds G . y = min ((h . [x,y]),(g . [y,z])) ) implies F = G )
assume that
A20: for y being Element of C2 holds F . y = min ((h . [x,y]),(g . [y,z])) and
A21: for y being Element of C2 holds G . y = min ((h . [x,y]),(g . [y,z])) ; ::_thesis: F = G
A22: for y being Element of C2 st y in C2 holds
F . y = G . y
proof
let y be Element of C2; ::_thesis: ( y in C2 implies F . y = G . y )
 F . y = min ((h . [x,y]),(g . [y,z])) by A20;
hence  ( y in C2 implies F . y = G . y ) by A21; ::_thesis: verum
end;
A23: dom G = C2 by FUNCT_2:def_1;
 dom F = C2 by FUNCT_2:def_1;
hence  F = G by A23, A22, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines min FUZZY_4:def_2_:_
 for C1, C2, C3 being non empty set
for h being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
for b8 being Membership_Func of C2 holds
( b8 = min (h,g,x,z) iff for y being Element of C2 holds b8 . y = min ((h . [x,y]),(g . [y,z])) );

definition
let C1, C2, C3 be non empty set ;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
funch (#) g ->  RMembership_Func of C1,C3 means :Def3: :: FUZZY_4:def 3
 for x, z being set st [x,z] in [:C1,C3:] holds
it . (x,z) = upper_bound (rng (min (h,g,x,z)));
existence
 ex b1 being RMembership_Func of C1,C3 st
for x, z being set st [x,z] in [:C1,C3:] holds
b1 . (x,z) = upper_bound (rng (min (h,g,x,z)))
proof
defpred S1[ set , set , set ] means $3 = upper_bound (rng (min (h,g,$1,$2)));
A1: for x, z, c1, c2 being set st x in C1 & z in C3 & S1[x,z,c1] & S1[x,z,c2] holds
c1 = c2 ;
A2: for x, z, c being set st x in C1 & z in C3 & S1[x,z,c] holds
c in REAL ;
consider IT being PartFunc of [:C1,C3:],REAL such that
A3: ( ( for x, z being set holds
( [x,z] in dom IT iff ( x in C1 & z in C3 & ex c being set st S1[x,z,c] ) ) ) & ( for x, z being set st [x,z] in dom IT holds
S1[x,z,IT . (x,z)] ) ) from BINOP_1:sch_5(A2, A1);
A4: [:C1,C3:] c= dom IT
proof
let x, z be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,z] in [:C1,C3:] or [x,z] in dom IT )
A5: ex c being set st c = upper_bound (rng (min (h,g,x,z))) ;
assume A6: [x,z] in [:C1,C3:] ; ::_thesis: [x,z] in dom IT
then A7: z in C3 by ZFMISC_1:87;
 x in C1 by A6, ZFMISC_1:87;
hence  [x,z] in dom IT by A3, A7, A5; ::_thesis: verum
end;
then A8: dom IT = [:C1,C3:] by XBOOLE_0:def_10;
A9: dom IT = [:C1,C3:] by A4, XBOOLE_0:def_10;
 rng IT c= [.0,1.]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in rng IT or c in [.0,1.] )
assume  c in rng IT ; ::_thesis: c in [.0,1.]
then consider a being Element of [:C1,C3:] such that
 a in dom IT and
A10: c = IT . a by PARTFUN1:3;
A11: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A12: 0 = lower_bound A by INTEGRA1:5;
A13: for x, z being set holds
( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (rng (min (h,g,x,z))) <= 1 )
proof
let x, z be set ; ::_thesis: ( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (rng (min (h,g,x,z))) <= 1 )
A14: rng (min (h,g,x,z)) c= A by RELAT_1:def_19;
 A is bounded_below by INTEGRA1:3;
then A15: lower_bound A <= lower_bound (rng (min (h,g,x,z))) by A14, SEQ_4:47;
 A is bounded_above by INTEGRA1:3;
then A16: upper_bound (rng (min (h,g,x,z))) <= upper_bound A by A14, SEQ_4:48;
 lower_bound (rng (min (h,g,x,z))) <= upper_bound (rng (min (h,g,x,z))) by Th1, SEQ_4:11;
hence  ( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (rng (min (h,g,x,z))) <= 1 ) by A11, A16, A15, INTEGRA1:5; ::_thesis: verum
end;
consider x, z being set  such that
 x in C1 and
 z in C3 and
A17: a = [x,z] by ZFMISC_1:def_2;
A18: IT . (x,z) = upper_bound (rng (min (h,g,x,z))) by A3, A9, A17;
then A19: IT . a <= 1 by A13, A17;
A20: 1 = upper_bound A by A11, INTEGRA1:5;
 0 <= IT . a by A13, A17, A18;
hence  c in [.0,1.] by A10, A12, A20, A19, INTEGRA2:1; ::_thesis: verum
end;
then  IT is RMembership_Func of C1,C3 by A8, FUNCT_2:def_1, RELAT_1:def_19;
hence  ex b1 being RMembership_Func of C1,C3 st
for x, z being set st [x,z] in [:C1,C3:] holds
b1 . (x,z) = upper_bound (rng (min (h,g,x,z))) by A3, A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being RMembership_Func of C1,C3 st ( for x, z being set st [x,z] in [:C1,C3:] holds
b1 . (x,z) = upper_bound (rng (min (h,g,x,z))) ) & ( for x, z being set st [x,z] in [:C1,C3:] holds
b2 . (x,z) = upper_bound (rng (min (h,g,x,z))) ) holds
b1 = b2
proof
let F, G be RMembership_Func of C1,C3; ::_thesis: ( ( for x, z being set st [x,z] in [:C1,C3:] holds
F . (x,z) = upper_bound (rng (min (h,g,x,z))) ) & ( for x, z being set st [x,z] in [:C1,C3:] holds
G . (x,z) = upper_bound (rng (min (h,g,x,z))) ) implies F = G )
assume that
A21: for x, z being set st [x,z] in [:C1,C3:] holds
F . (x,z) = upper_bound (rng (min (h,g,x,z))) and
A22: for x, z being set st [x,z] in [:C1,C3:] holds
G . (x,z) = upper_bound (rng (min (h,g,x,z))) ; ::_thesis: F = G
A23: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
F . c = G . c
proof
let c be Element of [:C1,C3:]; ::_thesis: ( c in [:C1,C3:] implies F . c = G . c )
consider x, z being set  such that
 x in C1 and
 z in C3 and
A24: c = [x,z] by ZFMISC_1:def_2;
A25: G . (x,z) = upper_bound (rng (min (h,g,x,z))) by A22, A24;
 F . (x,z) = upper_bound (rng (min (h,g,x,z))) by A21, A24;
hence  ( c in [:C1,C3:] implies F . c = G . c ) by A24, A25; ::_thesis: verum
end;
A26: dom G = [:C1,C3:] by FUNCT_2:def_1;
 dom F = [:C1,C3:] by FUNCT_2:def_1;
hence  F = G by A26, A23, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines (#) FUZZY_4:def_3_:_
 for C1, C2, C3 being non empty set
for h being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for b6 being RMembership_Func of C1,C3 holds
( b6 = h (#) g iff for x, z being set st [x,z] in [:C1,C3:] holds
b6 . (x,z) = upper_bound (rng (min (h,g,x,z))) );

Lm1:  for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
let f be RMembership_Func of C1,C2; ::_thesis: for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
let g, h be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
A3: for y being Element of C2 st y in C2 holds
(max ((min (f,g,x,z)),(min (f,h,x,z)))) . y = (min (f,(max (g,h)),x,z)) . y
proof
let y be Element of C2; ::_thesis: ( y in C2 implies (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y = (min (f,(max (g,h)),x,z)) . y )
assume  y in C2 ; ::_thesis: (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y = (min (f,(max (g,h)),x,z)) . y
A4: [y,z] in [:C2,C3:] by A2, ZFMISC_1:87;
(max ((min (f,g,x,z)),(min (f,h,x,z)))) . y = max (((min (f,g,x,z)) . y),((min (f,h,x,z)) . y)) by FUZZY_1:def_4
.= max (((min (f,g,x,z)) . y),(min ((f . [x,y]),(h . [y,z])))) by A1, A2, Def2
.= max ((min ((f . [x,y]),(g . [y,z]))),(min ((f . [x,y]),(h . [y,z])))) by A1, A2, Def2
.= min ((f . [x,y]),(max ((g . [y,z]),(h . [y,z])))) by XXREAL_0:38
.= min ((f . [x,y]),((max (g,h)) . [y,z])) by A4, FUZZY_1:def_4
.= (min (f,(max (g,h)),x,z)) . y by A1, A2, Def2 ;
hence  (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y = (min (f,(max (g,h)),x,z)) . y ; ::_thesis: verum
end;
set F = min (f,g,x,z);
set G = min (f,h,x,z);
A5: dom (min (f,(max (g,h)),x,z)) = C2 by FUNCT_2:def_1;
 rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) is real-bounded by Th1;
then A6: rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) is bounded_above by XXREAL_2:def_11;
A7: for s being real number st 0 < s holds
ex y being set st
( y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) & (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) & (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) & (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y )
then consider r being real number  such that
A8: r in rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) and
A9: (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < r by A6, SEQ_4:def_1;
 ex y being set st
( y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) & r = (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y ) by A8, FUNCT_1:def_3;
hence  ex y being set st
( y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) & (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y ) by A9; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
then consider y being set  such that
A10: y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) and
A11: (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y by A7;
A12: (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y = max (((min (f,g,x,z)) . y),((min (f,h,x,z)) . y)) by A10, FUZZY_1:def_4;
A13: for y being set st y in C2 holds
( (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) & (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) )
proof
let y be set ; ::_thesis: ( y in C2 implies ( (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) & (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) ) )
assume A14: y in C2 ; ::_thesis: ( (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) & (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) )
then  y in dom (min (f,h,x,z)) by FUNCT_2:def_1;
then A15: (min (f,h,x,z)) . y in rng (min (f,h,x,z)) by FUNCT_1:def_3;
 rng (min (f,h,x,z)) is real-bounded by Th1;
then A16: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def_11;
 rng (min (f,g,x,z)) is real-bounded by Th1;
then A17: rng (min (f,g,x,z)) is bounded_above by XXREAL_2:def_11;
 y in dom (min (f,g,x,z)) by A14, FUNCT_2:def_1;
then  (min (f,g,x,z)) . y in rng (min (f,g,x,z)) by FUNCT_1:def_3;
hence  ( (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) & (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) ) by A15, A17, A16, SEQ_4:def_1; ::_thesis: verum
end;
then A18: (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A10;
 (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) by A10, A13;
then  (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A12, A18, XXREAL_0:26;
hence  (upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s < max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A11, XXREAL_0:2; ::_thesis: verum
end;
then  for s being real number st 0 < s holds
(upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))) - s <= max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) ;
then A19: upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) <= max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by XREAL_1:57;
A20: for y being set st y in C2 holds
(max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))
proof
let y be set ; ::_thesis: ( y in C2 implies (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) )
assume  y in C2 ; ::_thesis: (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))
then  y in dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) by FUNCT_2:def_1;
then A21: (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y in rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) by FUNCT_1:def_3;
 rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) is real-bounded by Th1;
then  rng (max ((min (f,g,x,z)),(min (f,h,x,z)))) is bounded_above by XXREAL_2:def_11;
hence  (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by A21, SEQ_4:def_1; ::_thesis: verum
end;
 rng (min (f,h,x,z)) is real-bounded by Th1;
then A22: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def_11;
A23: for s being real number st 0 < s holds
ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s < (min (f,h,x,z)) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s < (min (f,h,x,z)) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s < (min (f,h,x,z)) . y )
then consider r being real number  such that
A24: r in rng (min (f,h,x,z)) and
A25: (upper_bound (rng (min (f,h,x,z)))) - s < r by A22, SEQ_4:def_1;
 ex y being set st
( y in dom (min (f,h,x,z)) & r = (min (f,h,x,z)) . y ) by A24, FUNCT_1:def_3;
hence  ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s < (min (f,h,x,z)) . y ) by A25; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))
then consider y being set  such that
A26: y in dom (min (f,h,x,z)) and
A27: (upper_bound (rng (min (f,h,x,z)))) - s < (min (f,h,x,z)) . y by A23;
 (min (f,h,x,z)) . y <= max (((min (f,g,x,z)) . y),((min (f,h,x,z)) . y)) by XXREAL_0:25;
then  (min (f,h,x,z)) . y <= (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y by A26, FUZZY_1:def_4;
then A28: (upper_bound (rng (min (f,h,x,z)))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y by A27, XXREAL_0:2;
 (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by A20, A26;
hence  (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by A28, XXREAL_0:2; ::_thesis: verum
end;
then A29: upper_bound (rng (min (f,h,x,z))) <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by XREAL_1:57;
 rng (min (f,g,x,z)) is real-bounded by Th1;
then A30: rng (min (f,g,x,z)) is bounded_above by XXREAL_2:def_11;
A31: for s being real number st 0 < s holds
ex y being set st
( y in dom (min (f,g,x,z)) & (upper_bound (rng (min (f,g,x,z)))) - s < (min (f,g,x,z)) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min (f,g,x,z)) & (upper_bound (rng (min (f,g,x,z)))) - s < (min (f,g,x,z)) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min (f,g,x,z)) & (upper_bound (rng (min (f,g,x,z)))) - s < (min (f,g,x,z)) . y )
then consider r being real number  such that
A32: r in rng (min (f,g,x,z)) and
A33: (upper_bound (rng (min (f,g,x,z)))) - s < r by A30, SEQ_4:def_1;
 ex y being set st
( y in dom (min (f,g,x,z)) & r = (min (f,g,x,z)) . y ) by A32, FUNCT_1:def_3;
hence  ex y being set st
( y in dom (min (f,g,x,z)) & (upper_bound (rng (min (f,g,x,z)))) - s < (min (f,g,x,z)) . y ) by A33; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z)))))
then consider y being set  such that
A34: y in dom (min (f,g,x,z)) and
A35: (upper_bound (rng (min (f,g,x,z)))) - s < (min (f,g,x,z)) . y by A31;
 (min (f,g,x,z)) . y <= max (((min (f,g,x,z)) . y),((min (f,h,x,z)) . y)) by XXREAL_0:25;
then  (min (f,g,x,z)) . y <= (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y by A34, FUZZY_1:def_4;
then A36: (upper_bound (rng (min (f,g,x,z)))) - s < (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y by A35, XXREAL_0:2;
 (max ((min (f,g,x,z)),(min (f,h,x,z)))) . y <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by A20, A34;
hence  (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by A36, XXREAL_0:2; ::_thesis: verum
end;
then  upper_bound (rng (min (f,g,x,z))) <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by XREAL_1:57;
then  max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) <= upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) by A29, XXREAL_0:28;
then A37: upper_bound (rng (max ((min (f,g,x,z)),(min (f,h,x,z))))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A19, XXREAL_0:1;
 dom (max ((min (f,g,x,z)),(min (f,h,x,z)))) = C2 by FUNCT_2:def_1;
hence  upper_bound (rng (min (f,(max (g,h)),x,z))) = max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A5, A3, A37, PARTFUN1:5; ::_thesis: verum
end;

theorem :: FUZZY_4:13
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds f (#) (max (g,h)) = max ((f (#) g),(f (#) h))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds f (#) (max (g,h)) = max ((f (#) g),(f (#) h))
let f be RMembership_Func of C1,C2; ::_thesis: for g, h being RMembership_Func of C2,C3 holds f (#) (max (g,h)) = max ((f (#) g),(f (#) h))
let g, h be RMembership_Func of C2,C3; ::_thesis: f (#) (max (g,h)) = max ((f (#) g),(f (#) h))
A1: dom (max ((f (#) g),(f (#) h))) = [:C1,C3:] by FUNCT_2:def_1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
(f (#) (max (g,h))) . c = (max ((f (#) g),(f (#) h))) . c
proof
let c be Element of [:C1,C3:]; ::_thesis: ( c in [:C1,C3:] implies (f (#) (max (g,h))) . c = (max ((f (#) g),(f (#) h))) . c )
consider x, z being set  such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def_2;
(f (#) (max (g,h))) . c = (f (#) (max (g,h))) . (x,z) by A5
.= upper_bound (rng (min (f,(max (g,h)),x,z))) by A5, Def3
.= max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A3, A4, Lm1
.= max (((f (#) g) . (x,z)),(upper_bound (rng (min (f,h,x,z))))) by A5, Def3
.= max (((f (#) g) . (x,z)),((f (#) h) . (x,z))) by A5, Def3
.= (max ((f (#) g),(f (#) h))) . c by A5, FUZZY_1:def_4 ;
hence  ( c in [:C1,C3:] implies (f (#) (max (g,h))) . c = (max ((f (#) g),(f (#) h))) . c ) ; ::_thesis: verum
end;
 dom (f (#) (max (g,h))) = [:C1,C3:] by FUNCT_2:def_1;
hence  f (#) (max (g,h)) = max ((f (#) g),(f (#) h)) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

Lm2:  for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let f, g be RMembership_Func of C1,C2; ::_thesis: for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let h be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
A3: for y being Element of C2 st y in C2 holds
(min ((max (f,g)),h,x,z)) . y = (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y
proof
let y be Element of C2; ::_thesis: ( y in C2 implies (min ((max (f,g)),h,x,z)) . y = (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )
assume  y in C2 ; ::_thesis: (min ((max (f,g)),h,x,z)) . y = (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y
A4: [x,y] in [:C1,C2:] by A1, ZFMISC_1:87;
(min ((max (f,g)),h,x,z)) . y = min (((max (f,g)) . [x,y]),(h . [y,z])) by A1, A2, Def2
.= min ((max ((f . [x,y]),(g . [x,y]))),(h . [y,z])) by A4, FUZZY_1:def_4
.= max ((min ((f . [x,y]),(h . [y,z]))),(min ((g . [x,y]),(h . [y,z])))) by XXREAL_0:38
.= max ((min ((f . [x,y]),(h . [y,z]))),((min (g,h,x,z)) . y)) by A1, A2, Def2
.= max (((min (f,h,x,z)) . y),((min (g,h,x,z)) . y)) by A1, A2, Def2 ;
hence  (min ((max (f,g)),h,x,z)) . y = (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y by FUZZY_1:def_4; ::_thesis: verum
end;
set F = min (f,h,x,z);
set G = min (g,h,x,z);
A5: dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) = C2 by FUNCT_2:def_1;
 rng (max ((min (f,h,x,z)),(min (g,h,x,z)))) is real-bounded by Th1;
then A6: rng (max ((min (f,h,x,z)),(min (g,h,x,z)))) is bounded_above by XXREAL_2:def_11;
A7: for y being set st y in dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) holds
(max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))
proof
let y be set ; ::_thesis: ( y in dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) implies (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) )
assume  y in dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) ; ::_thesis: (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))
then  (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y in rng (max ((min (f,h,x,z)),(min (g,h,x,z)))) by FUNCT_1:def_3;
hence  (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A6, SEQ_4:def_1; ::_thesis: verum
end;
 rng (min (g,h,x,z)) is real-bounded by Th1;
then A8: rng (min (g,h,x,z)) is bounded_above by XXREAL_2:def_11;
A9: for y being set st y in dom (min (g,h,x,z)) holds
(min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
proof
let y be set ; ::_thesis: ( y in dom (min (g,h,x,z)) implies (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) )
assume  y in dom (min (g,h,x,z)) ; ::_thesis: (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
then  (min (g,h,x,z)) . y in rng (min (g,h,x,z)) by FUNCT_1:def_3;
hence  (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) by A8, SEQ_4:def_1; ::_thesis: verum
end;
A10: for s being real number st 0 < s holds
ex y being set st
( y in dom (min (g,h,x,z)) & (upper_bound (rng (min (g,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min (g,h,x,z)) & (upper_bound (rng (min (g,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min (g,h,x,z)) & (upper_bound (rng (min (g,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )
then consider r being real number  such that
A11: r in rng (min (g,h,x,z)) and
A12: (upper_bound (rng (min (g,h,x,z)))) - s < r by A8, SEQ_4:def_1;
consider y being set  such that
A13: y in dom (min (g,h,x,z)) and
A14: r = (min (g,h,x,z)) . y by A11, FUNCT_1:def_3;
 (min (g,h,x,z)) . y <= max (((min (f,h,x,z)) . y),((min (g,h,x,z)) . y)) by XXREAL_0:25;
then  r <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y by A13, A14, FUZZY_1:def_4;
hence  ex y being set st
( y in dom (min (g,h,x,z)) & (upper_bound (rng (min (g,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y ) by A12, A13, XXREAL_0:2; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min (g,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (g,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min (g,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))
then consider y being set  such that
A15: y in dom (min (g,h,x,z)) and
A16: (upper_bound (rng (min (g,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y by A10;
 y in C2 by A15;
then  y in dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) by FUNCT_2:def_1;
then  (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A7;
hence  (upper_bound (rng (min (g,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A16, XXREAL_0:2; ::_thesis: verum
end;
then A17: upper_bound (rng (min (g,h,x,z))) <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by XREAL_1:57;
 rng (min (f,h,x,z)) is real-bounded by Th1;
then A18: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def_11;
A19: for s being real number st 0 < s holds
ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y )
then consider r being real number  such that
A20: r in rng (min (f,h,x,z)) and
A21: (upper_bound (rng (min (f,h,x,z)))) - s < r by A18, SEQ_4:def_1;
consider y being set  such that
A22: y in dom (min (f,h,x,z)) and
A23: r = (min (f,h,x,z)) . y by A20, FUNCT_1:def_3;
 (min (f,h,x,z)) . y <= max (((min (f,h,x,z)) . y),((min (g,h,x,z)) . y)) by XXREAL_0:25;
then  r <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y by A22, A23, FUZZY_1:def_4;
hence  ex y being set st
( y in dom (min (f,h,x,z)) & (upper_bound (rng (min (f,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y ) by A21, A22, XXREAL_0:2; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))
then consider y being set  such that
A24: y in dom (min (f,h,x,z)) and
A25: (upper_bound (rng (min (f,h,x,z)))) - s <= (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y by A19;
 y in C2 by A24;
then  y in dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) by FUNCT_2:def_1;
then  (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A7;
hence  (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by A25, XXREAL_0:2; ::_thesis: verum
end;
then  upper_bound (rng (min (f,h,x,z))) <= upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) by XREAL_1:57;
then A26: upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) >= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A17, XXREAL_0:28;
A27: for y being set st y in dom (min (f,h,x,z)) holds
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
proof
let y be set ; ::_thesis: ( y in dom (min (f,h,x,z)) implies (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) )
assume  y in dom (min (f,h,x,z)) ; ::_thesis: (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
then  (min (f,h,x,z)) . y in rng (min (f,h,x,z)) by FUNCT_1:def_3;
hence  (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A18, SEQ_4:def_1; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
then consider r being real number  such that
A28: r in rng (max ((min (f,h,x,z)),(min (g,h,x,z)))) and
A29: (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s < r by A6, SEQ_4:def_1;
consider y being set  such that
A30: y in dom (max ((min (f,h,x,z)),(min (g,h,x,z)))) and
A31: r = (max ((min (f,h,x,z)),(min (g,h,x,z)))) . y by A28, FUNCT_1:def_3;
A32: y in C2 by A30;
then  y in dom (min (g,h,x,z)) by FUNCT_2:def_1;
then A33: (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) by A9;
 y in dom (min (f,h,x,z)) by A32, FUNCT_2:def_1;
then  (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A27;
then A34: max (((min (f,h,x,z)) . y),((min (g,h,x,z)) . y)) <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A33, XXREAL_0:26;
 (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s <= max (((min (f,h,x,z)) . y),((min (g,h,x,z)) . y)) by A29, A30, A31, FUZZY_1:def_4;
hence  (upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z)))))) - s <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A34, XXREAL_0:2; ::_thesis: verum
end;
then A35: upper_bound (rng (max ((min (f,h,x,z)),(min (g,h,x,z))))) <= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by XREAL_1:57;
 dom (min ((max (f,g)),h,x,z)) = C2 by FUNCT_2:def_1;
then  min ((max (f,g)),h,x,z) = max ((min (f,h,x,z)),(min (g,h,x,z))) by A5, A3, PARTFUN1:5;
hence  upper_bound (rng (min ((max (f,g)),h,x,z))) = max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A35, A26, XXREAL_0:1; ::_thesis: verum
end;

theorem :: FUZZY_4:14
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds (max (f,g)) (#) h = max ((f (#) h),(g (#) h))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds (max (f,g)) (#) h = max ((f (#) h),(g (#) h))
let f, g be RMembership_Func of C1,C2; ::_thesis: for h being RMembership_Func of C2,C3 holds (max (f,g)) (#) h = max ((f (#) h),(g (#) h))
let h be RMembership_Func of C2,C3; ::_thesis: (max (f,g)) (#) h = max ((f (#) h),(g (#) h))
A1: dom (max ((f (#) h),(g (#) h))) = [:C1,C3:] by FUNCT_2:def_1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
((max (f,g)) (#) h) . c = (max ((f (#) h),(g (#) h))) . c
proof
let c be Element of [:C1,C3:]; ::_thesis: ( c in [:C1,C3:] implies ((max (f,g)) (#) h) . c = (max ((f (#) h),(g (#) h))) . c )
consider x, z being set  such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def_2;
((max (f,g)) (#) h) . c = ((max (f,g)) (#) h) . (x,z) by A5
.= upper_bound (rng (min ((max (f,g)),h,x,z))) by A5, Def3
.= max ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A3, A4, Lm2
.= max (((f (#) h) . (x,z)),(upper_bound (rng (min (g,h,x,z))))) by A5, Def3
.= max (((f (#) h) . (x,z)),((g (#) h) . (x,z))) by A5, Def3
.= (max ((f (#) h),(g (#) h))) . c by A5, FUZZY_1:def_4 ;
hence  ( c in [:C1,C3:] implies ((max (f,g)) (#) h) . c = (max ((f (#) h),(g (#) h))) . c ) ; ::_thesis: verum
end;
 dom ((max (f,g)) (#) h) = [:C1,C3:] by FUNCT_2:def_1;
hence  (max (f,g)) (#) h = max ((f (#) h),(g (#) h)) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

Lm3:  for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
let f be RMembership_Func of C1,C2; ::_thesis: for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
let g, h be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z)))))
set F = min (f,(min (g,h)),x,z);
set G = min (f,g,x,z);
set H = min (f,h,x,z);
 rng (min (f,(min (g,h)),x,z)) is real-bounded by Th1;
then A3: rng (min (f,(min (g,h)),x,z)) is bounded_above by XXREAL_2:def_11;
A4: for s being real number st 0 < s holds
ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,g,x,z)) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,g,x,z)) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,g,x,z)) . y )
then consider r being real number  such that
A5: r in rng (min (f,(min (g,h)),x,z)) and
A6: (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A7: y in dom (min (f,(min (g,h)),x,z)) and
A8: r = (min (f,(min (g,h)),x,z)) . y by A5, FUNCT_1:def_3;
A9: [y,z] in [:C2,C3:] by A2, A7, ZFMISC_1:87;
(min (f,(min (g,h)),x,z)) . y = min ((f . [x,y]),((min (g,h)) . [y,z])) by A1, A2, A7, Def2
.= min ((f . [x,y]),(min ((g . [y,z]),(h . [y,z])))) by A9, FUZZY_1:def_3
.= min ((min ((f . [x,y]),(g . [y,z]))),(h . [y,z])) by XXREAL_0:33
.= min (((min (f,g,x,z)) . y),(h . [y,z])) by A1, A2, A7, Def2 ;
then  r <= (min (f,g,x,z)) . y by A8, XXREAL_0:17;
hence  ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,g,x,z)) . y ) by A6, A7, XXREAL_0:2; ::_thesis: verum
end;
A10: for s being real number st 0 < s holds
ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,h,x,z)) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,h,x,z)) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,h,x,z)) . y )
then consider r being real number  such that
A11: r in rng (min (f,(min (g,h)),x,z)) and
A12: (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A13: y in dom (min (f,(min (g,h)),x,z)) and
A14: r = (min (f,(min (g,h)),x,z)) . y by A11, FUNCT_1:def_3;
A15: [y,z] in [:C2,C3:] by A2, A13, ZFMISC_1:87;
(min (f,(min (g,h)),x,z)) . y = min ((f . [x,y]),((min (g,h)) . [y,z])) by A1, A2, A13, Def2
.= min ((f . [x,y]),(min ((g . [y,z]),(h . [y,z])))) by A15, FUZZY_1:def_3
.= min ((min ((f . [x,y]),(h . [y,z]))),(g . [y,z])) by XXREAL_0:33
.= min (((min (f,h,x,z)) . y),(g . [y,z])) by A1, A2, A13, Def2 ;
then  r <= (min (f,h,x,z)) . y by A14, XXREAL_0:17;
hence  ex y being set st
( y in dom (min (f,(min (g,h)),x,z)) & (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,h,x,z)) . y ) by A12, A13, XXREAL_0:2; ::_thesis: verum
end;
 rng (min (f,h,x,z)) is real-bounded by Th1;
then A16: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def_11;
A17: for y being set st y in dom (min (f,h,x,z)) holds
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
proof
let y be set ; ::_thesis: ( y in dom (min (f,h,x,z)) implies (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) )
assume  y in dom (min (f,h,x,z)) ; ::_thesis: (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
then  (min (f,h,x,z)) . y in rng (min (f,h,x,z)) by FUNCT_1:def_3;
hence  (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A16, SEQ_4:def_1; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,h,x,z))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
then consider y being set  such that
A18: y in dom (min (f,(min (g,h)),x,z)) and
A19: (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,h,x,z)) . y by A10;
 y in C2 by A18;
then  y in dom (min (f,h,x,z)) by FUNCT_2:def_1;
then  (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A17;
hence  (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,h,x,z))) by A19, XXREAL_0:2; ::_thesis: verum
end;
then A20: upper_bound (rng (min (f,(min (g,h)),x,z))) <= upper_bound (rng (min (f,h,x,z))) by XREAL_1:57;
 rng (min (f,g,x,z)) is real-bounded by Th1;
then A21: rng (min (f,g,x,z)) is bounded_above by XXREAL_2:def_11;
A22: for y being set st y in dom (min (f,g,x,z)) holds
(min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z)))
proof
let y be set ; ::_thesis: ( y in dom (min (f,g,x,z)) implies (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) )
assume  y in dom (min (f,g,x,z)) ; ::_thesis: (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z)))
then  (min (f,g,x,z)) . y in rng (min (f,g,x,z)) by FUNCT_1:def_3;
hence  (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) by A21, SEQ_4:def_1; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,g,x,z)))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,g,x,z))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,g,x,z)))
then consider y being set  such that
A23: y in dom (min (f,(min (g,h)),x,z)) and
A24: (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= (min (f,g,x,z)) . y by A4;
 y in C2 by A23;
then  y in dom (min (f,g,x,z)) by FUNCT_2:def_1;
then  (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) by A22;
hence  (upper_bound (rng (min (f,(min (g,h)),x,z)))) - s <= upper_bound (rng (min (f,g,x,z))) by A24, XXREAL_0:2; ::_thesis: verum
end;
then  upper_bound (rng (min (f,(min (g,h)),x,z))) <= upper_bound (rng (min (f,g,x,z))) by XREAL_1:57;
hence  upper_bound (rng (min (f,(min (g,h)),x,z))) <= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A20, XXREAL_0:20; ::_thesis: verum
end;

theorem :: FUZZY_4:15
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds min ((f (#) g),(f (#) h)) c=
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds min ((f (#) g),(f (#) h)) c=
let f be RMembership_Func of C1,C2; ::_thesis: for g, h being RMembership_Func of C2,C3 holds min ((f (#) g),(f (#) h)) c=
let g, h be RMembership_Func of C2,C3; ::_thesis: min ((f (#) g),(f (#) h)) c=
let c be Element of [:C1,C3:]; :: according to FUZZY_1:def_2 ::_thesis: (f (#) (min (g,h))) . c <= (min ((f (#) g),(f (#) h))) . c
consider x, z being set  such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def_2;
A4: (f (#) (min (g,h))) . (x,z) = upper_bound (rng (min (f,(min (g,h)),x,z))) by A3, Def3;
(min ((f (#) g),(f (#) h))) . (x,z) = min (((f (#) g) . (x,z)),((f (#) h) . (x,z))) by A3, FUZZY_1:def_3
.= min (((f (#) g) . (x,z)),(upper_bound (rng (min (f,h,x,z))))) by A3, Def3
.= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A3, Def3 ;
hence  (f (#) (min (g,h))) . c <= (min ((f (#) g),(f (#) h))) . c by A1, A2, A3, A4, Lm3; ::_thesis: verum
end;

Lm4:  for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let f, g be RMembership_Func of C1,C2; ::_thesis: for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let h be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z)))))
set F = min ((min (f,g)),h,x,z);
set G = min (f,h,x,z);
set H = min (g,h,x,z);
 rng (min ((min (f,g)),h,x,z)) is real-bounded by Th1;
then A3: rng (min ((min (f,g)),h,x,z)) is bounded_above by XXREAL_2:def_11;
A4: for s being real number st 0 < s holds
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y )
then consider r being real number  such that
A5: r in rng (min ((min (f,g)),h,x,z)) and
A6: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A7: y in dom (min ((min (f,g)),h,x,z)) and
A8: r = (min ((min (f,g)),h,x,z)) . y by A5, FUNCT_1:def_3;
A9: [x,y] in [:C1,C2:] by A1, A7, ZFMISC_1:87;
(min ((min (f,g)),h,x,z)) . y = min (((min (f,g)) . [x,y]),(h . [y,z])) by A1, A2, A7, Def2
.= min ((min ((f . [x,y]),(g . [x,y]))),(h . [y,z])) by A9, FUZZY_1:def_3
.= min ((min ((h . [y,z]),(f . [x,y]))),(g . [x,y])) by XXREAL_0:33
.= min (((min (f,h,x,z)) . y),(g . [x,y])) by A1, A2, A7, Def2 ;
then  r <= (min (f,h,x,z)) . y by A8, XXREAL_0:17;
hence  ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y ) by A6, A7, XXREAL_0:2; ::_thesis: verum
end;
A10: for s being real number st 0 < s holds
ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y ) )
assume  0 < s ; ::_thesis: ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y )
then consider r being real number  such that
A11: r in rng (min ((min (f,g)),h,x,z)) and
A12: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A13: y in dom (min ((min (f,g)),h,x,z)) and
A14: r = (min ((min (f,g)),h,x,z)) . y by A11, FUNCT_1:def_3;
A15: [x,y] in [:C1,C2:] by A1, A13, ZFMISC_1:87;
(min ((min (f,g)),h,x,z)) . y = min (((min (f,g)) . [x,y]),(h . [y,z])) by A1, A2, A13, Def2
.= min ((min ((f . [x,y]),(g . [x,y]))),(h . [y,z])) by A15, FUZZY_1:def_3
.= min ((f . [x,y]),(min ((h . [y,z]),(g . [x,y])))) by XXREAL_0:33
.= min (((min (g,h,x,z)) . y),(f . [x,y])) by A1, A2, A13, Def2 ;
then  r <= (min (g,h,x,z)) . y by A14, XXREAL_0:17;
hence  ex y being set st
( y in dom (min ((min (f,g)),h,x,z)) & (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y ) by A12, A13, XXREAL_0:2; ::_thesis: verum
end;
 rng (min (g,h,x,z)) is real-bounded by Th1;
then A16: rng (min (g,h,x,z)) is bounded_above by XXREAL_2:def_11;
A17: for y being set st y in dom (min (g,h,x,z)) holds
(min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
proof
let y be set ; ::_thesis: ( y in dom (min (g,h,x,z)) implies (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) )
assume  y in dom (min (g,h,x,z)) ; ::_thesis: (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z)))
then  (min (g,h,x,z)) . y in rng (min (g,h,x,z)) by FUNCT_1:def_3;
hence  (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) by A16, SEQ_4:def_1; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z)))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z)))
then consider y being set  such that
A18: y in dom (min ((min (f,g)),h,x,z)) and
A19: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (g,h,x,z)) . y by A10;
 y in C2 by A18;
then  y in dom (min (g,h,x,z)) by FUNCT_2:def_1;
then  (min (g,h,x,z)) . y <= upper_bound (rng (min (g,h,x,z))) by A17;
hence  (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (g,h,x,z))) by A19, XXREAL_0:2; ::_thesis: verum
end;
then A20: upper_bound (rng (min ((min (f,g)),h,x,z))) <= upper_bound (rng (min (g,h,x,z))) by XREAL_1:57;
 rng (min (f,h,x,z)) is real-bounded by Th1;
then A21: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def_11;
A22: for y being set st y in dom (min (f,h,x,z)) holds
(min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
proof
let y be set ; ::_thesis: ( y in dom (min (f,h,x,z)) implies (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) )
assume  y in dom (min (f,h,x,z)) ; ::_thesis: (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z)))
then  (min (f,h,x,z)) . y in rng (min (f,h,x,z)) by FUNCT_1:def_3;
hence  (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A21, SEQ_4:def_1; ::_thesis: verum
end;
 for s being real number st 0 < s holds
(upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z))) )
assume  0 < s ; ::_thesis: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z)))
then consider y being set  such that
A23: y in dom (min ((min (f,g)),h,x,z)) and
A24: (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= (min (f,h,x,z)) . y by A4;
 y in C2 by A23;
then  y in dom (min (f,h,x,z)) by FUNCT_2:def_1;
then  (min (f,h,x,z)) . y <= upper_bound (rng (min (f,h,x,z))) by A22;
hence  (upper_bound (rng (min ((min (f,g)),h,x,z)))) - s <= upper_bound (rng (min (f,h,x,z))) by A24, XXREAL_0:2; ::_thesis: verum
end;
then  upper_bound (rng (min ((min (f,g)),h,x,z))) <= upper_bound (rng (min (f,h,x,z))) by XREAL_1:57;
hence  upper_bound (rng (min ((min (f,g)),h,x,z))) <= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A20, XXREAL_0:20; ::_thesis: verum
end;

theorem :: FUZZY_4:16
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds min ((f (#) h),(g (#) h)) c=
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds min ((f (#) h),(g (#) h)) c=
let f, g be RMembership_Func of C1,C2; ::_thesis: for h being RMembership_Func of C2,C3 holds min ((f (#) h),(g (#) h)) c=
let h be RMembership_Func of C2,C3; ::_thesis: min ((f (#) h),(g (#) h)) c=
let c be Element of [:C1,C3:]; :: according to FUZZY_1:def_2 ::_thesis: ((min (f,g)) (#) h) . c <= (min ((f (#) h),(g (#) h))) . c
consider x, z being set  such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def_2;
A4: ((min (f,g)) (#) h) . (x,z) = upper_bound (rng (min ((min (f,g)),h,x,z))) by A3, Def3;
(min ((f (#) h),(g (#) h))) . (x,z) = min (((f (#) h) . (x,z)),((g (#) h) . (x,z))) by A3, FUZZY_1:def_3
.= min ((upper_bound (rng (min (f,h,x,z)))),((g (#) h) . (x,z))) by A3, Def3
.= min ((upper_bound (rng (min (f,h,x,z)))),(upper_bound (rng (min (g,h,x,z))))) by A3, Def3 ;
hence  ((min (f,g)) (#) h) . c <= (min ((f (#) h),(g (#) h))) . c by A1, A2, A3, A4, Lm4; ::_thesis: verum
end;

Lm5:  for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
let f be RMembership_Func of C1,C2; ::_thesis: for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
let g be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z))) )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
 rng (min (f,g,x,z)) is real-bounded by Th1;
then A3: rng (min (f,g,x,z)) is bounded_above by XXREAL_2:def_11;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x)))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x))) )
assume  s > 0 ; ::_thesis: (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x)))
then consider r being real number  such that
A4: r in rng (min (f,g,x,z)) and
A5: (upper_bound (rng (min (f,g,x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A6: y in dom (min (f,g,x,z)) and
A7: r = (min (f,g,x,z)) . y by A4, FUNCT_1:def_3;
A8: [z,y] in [:C3,C2:] by A2, A6, ZFMISC_1:87;
 y in C2 by A6;
then  y in dom (min ((converse g),(converse f),z,x)) by FUNCT_2:def_1;
then A9: (min ((converse g),(converse f),z,x)) . y <= upper_bound (rng (min ((converse g),(converse f),z,x))) by Th1;
A10: [y,x] in [:C2,C1:] by A1, A6, ZFMISC_1:87;
r = min ((f . (x,y)),(g . (y,z))) by A1, A2, A6, A7, Def2
.= min (((converse f) . (y,x)),(g . (y,z))) by A10, Def1
.= min (((converse f) . (y,x)),((converse g) . (z,y))) by A8, Def1
.= (min ((converse g),(converse f),z,x)) . y by A1, A2, A6, Def2 ;
hence  (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x))) by A5, A9, XXREAL_0:2; ::_thesis: verum
end;
then A11: upper_bound (rng (min ((converse g),(converse f),z,x))) >= upper_bound (rng (min (f,g,x,z))) by XREAL_1:57;
 rng (min ((converse g),(converse f),z,x)) is real-bounded by Th1;
then A12: rng (min ((converse g),(converse f),z,x)) is bounded_above by XXREAL_2:def_11;
 for s being real number st 0 < s holds
(upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z)))
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z))) )
assume  s > 0 ; ::_thesis: (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z)))
then consider r being real number  such that
A13: r in rng (min ((converse g),(converse f),z,x)) and
A14: (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s < r by A12, SEQ_4:def_1;
consider y being set  such that
A15: y in dom (min ((converse g),(converse f),z,x)) and
A16: r = (min ((converse g),(converse f),z,x)) . y by A13, FUNCT_1:def_3;
A17: [z,y] in [:C3,C2:] by A2, A15, ZFMISC_1:87;
 y in C2 by A15;
then  y in dom (min (f,g,x,z)) by FUNCT_2:def_1;
then A18: (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) by Th1;
A19: [y,x] in [:C2,C1:] by A1, A15, ZFMISC_1:87;
r = min (((converse g) . (z,y)),((converse f) . (y,x))) by A1, A2, A15, A16, Def2
.= min ((g . (y,z)),((converse f) . (y,x))) by A17, Def1
.= min ((g . (y,z)),(f . (x,y))) by A19, Def1
.= (min (f,g,x,z)) . y by A1, A2, A15, Def2 ;
hence  (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z))) by A14, A18, XXREAL_0:2; ::_thesis: verum
end;
then  upper_bound (rng (min ((converse g),(converse f),z,x))) <= upper_bound (rng (min (f,g,x,z))) by XREAL_1:57;
hence  upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z))) by A11, XXREAL_0:1; ::_thesis: verum
end;

theorem :: FUZZY_4:17
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3 holds converse (f (#) g) = (converse g) (#) (converse f)
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3 holds converse (f (#) g) = (converse g) (#) (converse f)
let f be RMembership_Func of C1,C2; ::_thesis: for g being RMembership_Func of C2,C3 holds converse (f (#) g) = (converse g) (#) (converse f)
let g be RMembership_Func of C2,C3; ::_thesis: converse (f (#) g) = (converse g) (#) (converse f)
A1: dom ((converse g) (#) (converse f)) = [:C3,C1:] by FUNCT_2:def_1;
A2: for c being Element of [:C3,C1:] st c in [:C3,C1:] holds
(converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c
proof
let c be Element of [:C3,C1:]; ::_thesis: ( c in [:C3,C1:] implies (converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c )
assume  c in [:C3,C1:] ; ::_thesis: (converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c
consider z, x being set  such that
A3: z in C3 and
A4: x in C1 and
A5: c = [z,x] by ZFMISC_1:def_2;
A6: [x,z] in [:C1,C3:] by A3, A4, ZFMISC_1:87;
A7: ((converse g) (#) (converse f)) . (z,x) = upper_bound (rng (min ((converse g),(converse f),z,x))) by A5, Def3;
(converse (f (#) g)) . (z,x) = (f (#) g) . (x,z) by A5, Def1
.= upper_bound (rng (min (f,g,x,z))) by A6, Def3 ;
hence  (converse (f (#) g)) . c = ((converse g) (#) (converse f)) . c by A3, A4, A5, A7, Lm5; ::_thesis: verum
end;
 dom (converse (f (#) g)) = [:C3,C1:] by FUNCT_2:def_1;
hence  converse (f (#) g) = (converse g) (#) (converse f) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

theorem Th18: :: FUZZY_4:18
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
let f, g be RMembership_Func of C1,C2; ::_thesis: for h, k being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
let h, k be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
let x, z be set ; ::_thesis: ( x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) implies (f (#) h) . [x,z] <= (g (#) k) . [x,z] )
assume that
A1: x in C1 and
A2: z in C3 and
A3: for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ; ::_thesis: (f (#) h) . [x,z] <= (g (#) k) . [x,z]
A4: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
then A5: (g (#) k) . (x,z) = upper_bound (rng (min (g,k,x,z))) by Def3;
 rng (min (f,h,x,z)) is real-bounded by Th1;
then A6: rng (min (f,h,x,z)) is bounded_above by XXREAL_2:def_11;
A7: for s being real number st s > 0 holds
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z)))
proof
let s be real number ; ::_thesis: ( s > 0 implies (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z))) )
assume  s > 0 ; ::_thesis: (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z)))
then consider r being real number  such that
A8: r in rng (min (f,h,x,z)) and
A9: (upper_bound (rng (min (f,h,x,z)))) - s < r by A6, SEQ_4:def_1;
consider y being set  such that
A10: y in dom (min (f,h,x,z)) and
A11: r = (min (f,h,x,z)) . y by A8, FUNCT_1:def_3;
A12: h . [y,z] <= k . [y,z] by A3, A10;
 f . [x,y] <= g . [x,y] by A3, A10;
then  min ((f . [x,y]),(h . [y,z])) <= min ((g . [x,y]),(k . [y,z])) by A12, XXREAL_0:18;
then A13: (min (f,h,x,z)) . y <= min ((g . [x,y]),(k . [y,z])) by A1, A2, A10, Def2;
 y in C2 by A10;
then A14: y in dom (min (g,k,x,z)) by FUNCT_2:def_1;
 min ((g . [x,y]),(k . [y,z])) = (min (g,k,x,z)) . y by A1, A2, A10, Def2;
then  min ((g . [x,y]),(k . [y,z])) <= upper_bound (rng (min (g,k,x,z))) by A14, Th1;
then  (min (f,h,x,z)) . y <= upper_bound (rng (min (g,k,x,z))) by A13, XXREAL_0:2;
hence  (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z))) by A9, A11, XXREAL_0:2; ::_thesis: verum
end;
 (f (#) h) . (x,z) = upper_bound (rng (min (f,h,x,z))) by A4, Def3;
hence  (f (#) h) . [x,z] <= (g (#) k) . [x,z] by A5, A7, XREAL_1:57; ::_thesis: verum
end;

theorem :: FUZZY_4:19
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3 st g c= & k c= holds
g (#) k c=
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3 st g c= & k c= holds
g (#) k c=
let f, g be RMembership_Func of C1,C2; ::_thesis: for h, k being RMembership_Func of C2,C3 st g c= & k c= holds
g (#) k c=
let h, k be RMembership_Func of C2,C3; ::_thesis: ( g c= & k c= implies g (#) k c= )
assume that
A1: g c= and
A2: k c= ; ::_thesis: g (#) k c=
let c be Element of [:C1,C3:]; :: according to FUZZY_1:def_2 ::_thesis: (f (#) h) . c <= (g (#) k) . c
consider x, z being set  such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def_2;
 for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] )
proof
let y be set ; ::_thesis: ( y in C2 implies ( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) )
assume A6: y in C2 ; ::_thesis: ( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] )
then A7: [y,z] in [:C2,C3:] by A4, ZFMISC_1:87;
 [x,y] in [:C1,C2:] by A3, A6, ZFMISC_1:87;
hence  ( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) by A1, A2, A7, FUZZY_1:def_2; ::_thesis: verum
end;
hence  (f (#) h) . c <= (g (#) k) . c by A3, A4, A5, Th18; ::_thesis: verum
end;

begin

definition
let C1, C2 be non empty set ;
func Imf (C1,C2) ->  RMembership_Func of C1,C2 means :Def4: :: FUZZY_4:def 4
 for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies it . (x,y) = 1 ) & ( x <> y implies it . (x,y) = 0 ) );
existence
 ex b1 being RMembership_Func of C1,C2 st
for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . (x,y) = 1 ) & ( x <> y implies b1 . (x,y) = 0 ) )
proof
defpred S1[ set , set , set ] means ( ( $1 = $2 implies $3 = 1 ) & ( not $1 = $2 implies $3 = 0 ) );
A1: for x, y, z1, z2 being set st x in C1 & y in C2 & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2 ;
A2: for x, y, z being set st x in C1 & y in C2 & S1[x,y,z] holds
z in REAL ;
consider IT being PartFunc of [:C1,C2:],REAL such that
A3: ( ( for x, y being set holds
( [x,y] in dom IT iff ( x in C1 & y in C2 & ex z being set st S1[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom IT holds
S1[x,y,IT . (x,y)] ) ) from BINOP_1:sch_5(A2, A1);
 [:C1,C2:] c= dom IT
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in [:C1,C2:] or [x,y] in dom IT )
A4: ( not x = y implies ex z being set st
( ( x = y implies z = 1 ) & ( not x = y implies z = 0 ) ) ) ;
assume A5: [x,y] in [:C1,C2:] ; ::_thesis: [x,y] in dom IT
then A6: y in C2 by ZFMISC_1:87;
 x in C1 by A5, ZFMISC_1:87;
hence  [x,y] in dom IT by A3, A6, A4; ::_thesis: verum
end;
then A7: dom IT = [:C1,C2:] by XBOOLE_0:def_10;
 rng IT c= [.0,1.]
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in rng IT or c in [.0,1.] )
assume  c in rng IT ; ::_thesis: c in [.0,1.]
then consider z being Element of [:C1,C2:] such that
A8: z in dom IT and
A9: c = IT . z by PARTFUN1:3;
consider x, y being set  such that
 x in C1 and
 y in C2 and
A10: z = [x,y] by ZFMISC_1:def_2;
A11: ( 1 in [.0,1.] & 0 in [.0,1.] )
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A13: 1 = upper_bound A by INTEGRA1:5;
 0 = lower_bound A by A12, INTEGRA1:5;
hence  ( 1 in [.0,1.] & 0 in [.0,1.] ) by A13, INTEGRA2:1; ::_thesis: verum
end;
then A14: ( x <> y implies IT . (x,y) in [.0,1.] ) by A3, A8, A10;
 ( x = y implies IT . (x,y) in [.0,1.] ) by A3, A8, A10, A11;
hence  c in [.0,1.] by A9, A10, A14; ::_thesis: verum
end;
then  IT is RMembership_Func of C1,C2 by A7, FUNCT_2:def_1, RELAT_1:def_19;
hence  ex b1 being RMembership_Func of C1,C2 st
for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . (x,y) = 1 ) & ( x <> y implies b1 . (x,y) = 0 ) ) by A3, A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being RMembership_Func of C1,C2 st ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . (x,y) = 1 ) & ( x <> y implies b1 . (x,y) = 0 ) ) ) & ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b2 . (x,y) = 1 ) & ( x <> y implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
proof
let F, G be RMembership_Func of C1,C2; ::_thesis: ( ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies F . (x,y) = 1 ) & ( x <> y implies F . (x,y) = 0 ) ) ) & ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies G . (x,y) = 1 ) & ( x <> y implies G . (x,y) = 0 ) ) ) implies F = G )
assume that
A15: for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies F . (x,y) = 1 ) & ( x <> y implies F . (x,y) = 0 ) ) and
A16: for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies G . (x,y) = 1 ) & ( x <> y implies G . (x,y) = 0 ) ) ; ::_thesis: F = G
A17: for x, y being set st x in C1 & y in C2 holds
F . (x,y) = G . (x,y)
proof
let x, y be set ; ::_thesis: ( x in C1 & y in C2 implies F . (x,y) = G . (x,y) )
assume that
A18: x in C1 and
A19: y in C2 ; ::_thesis: F . (x,y) = G . (x,y)
A20: [x,y] in [:C1,C2:] by A18, A19, ZFMISC_1:87;
then A21: ( not x = y implies F . (x,y) = 0 ) by A15;
 ( x = y implies F . (x,y) = 1 ) by A15, A20;
hence  F . (x,y) = G . (x,y) by A16, A20, A21; ::_thesis: verum
end;
A22: dom G = [:C1,C2:] by FUNCT_2:def_1;
 dom F = [:C1,C2:] by FUNCT_2:def_1;
hence  F = G by A22, A17, FUNCT_3:6; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Imf FUZZY_4:def_4_:_
 for C1, C2 being non empty set
for b3 being RMembership_Func of C1,C2 holds
( b3 = Imf (C1,C2) iff for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b3 . (x,y) = 1 ) & ( x <> y implies b3 . (x,y) = 0 ) ) );

theorem :: FUZZY_4:20
for C1, C2 being non empty set
for c being Element of [:C1,C2:] holds
( (Zmf (C1,C2)) . c = 0 & (Umf (C1,C2)) . c = 1 ) by FUNCT_3:def_3;

theorem :: FUZZY_4:21
for C1, C2 being non empty set
for x, y being set st [x,y] in [:C1,C2:] holds
( (Zmf (C1,C2)) . [x,y] = 0 & (Umf (C1,C2)) . [x,y] = 1 ) by FUNCT_3:def_3;

Lm6:  for C2, C3, C1 being non empty set
for f being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
proof
let C2, C3, C1 be non empty set ; ::_thesis: for f being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
let f be RMembership_Func of C2,C3; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z] )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
 rng (min ((Zmf (C1,C2)),f,x,z)) is real-bounded by Th1;
then A3: rng (min ((Zmf (C1,C2)),f,x,z)) is bounded_above by XXREAL_2:def_11;
 for s being real number st 0 < s holds
(upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z]
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z] )
assume  s > 0 ; ::_thesis: (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z]
then consider r being real number  such that
A4: r in rng (min ((Zmf (C1,C2)),f,x,z)) and
A5: (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A6: y in dom (min ((Zmf (C1,C2)),f,x,z)) and
A7: r = (min ((Zmf (C1,C2)),f,x,z)) . y by A4, FUNCT_1:def_3;
A8: [x,y] in [:C1,C2:] by A1, A6, ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
A10: 0 <= f . [y,z] by Th3;
r = min (((Zmf (C1,C2)) . [x,y]),(f . [y,z])) by A1, A2, A6, A7, Def2
.= min (0,(f . [y,z])) by A8, FUNCT_3:def_3
.= 0 by A10, XXREAL_0:def_9
.= (Zmf (C1,C3)) . [x,z] by A9, FUNCT_3:def_3 ;
hence  (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z] by A5; ::_thesis: verum
end;
then A11: upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) <= (Zmf (C1,C3)) . [x,z] by XREAL_1:57;
 upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) >= (Zmf (C1,C3)) . [x,z]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
 rng (min ((Zmf (C1,C2)),f,x,z)) c= [.0,1.] by RELAT_1:def_19;
then A13: lower_bound A <= lower_bound (rng (min ((Zmf (C1,C2)),f,x,z))) by A12, SEQ_4:47;
 A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A14: 0 = lower_bound A by INTEGRA1:5;
A15: lower_bound (rng (min ((Zmf (C1,C2)),f,x,z))) <= upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) by Th1, SEQ_4:11;
 [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
hence  upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) >= (Zmf (C1,C3)) . [x,z] by A14, A13, A15, FUNCT_3:def_3; ::_thesis: verum
end;
hence  upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z] by A11, XXREAL_0:1; ::_thesis: verum
end;

theorem Th22: :: FUZZY_4:22
for C2, C3, C1 being non empty set
for f being RMembership_Func of C2,C3 holds (Zmf (C1,C2)) (#) f = Zmf (C1,C3)
proof
let C2, C3, C1 be non empty set ; ::_thesis: for f being RMembership_Func of C2,C3 holds (Zmf (C1,C2)) (#) f = Zmf (C1,C3)
let f be RMembership_Func of C2,C3; ::_thesis: (Zmf (C1,C2)) (#) f = Zmf (C1,C3)
A1: dom (Zmf (C1,C3)) = [:C1,C3:] by FUNCT_2:def_1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
((Zmf (C1,C2)) (#) f) . c = (Zmf (C1,C3)) . c
proof
let c be Element of [:C1,C3:]; ::_thesis: ( c in [:C1,C3:] implies ((Zmf (C1,C2)) (#) f) . c = (Zmf (C1,C3)) . c )
consider x, z being set  such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def_2;
((Zmf (C1,C2)) (#) f) . c = ((Zmf (C1,C2)) (#) f) . (x,z) by A5
.= upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) by A5, Def3
.= (Zmf (C1,C3)) . c by A3, A4, A5, Lm6 ;
hence  ( c in [:C1,C3:] implies ((Zmf (C1,C2)) (#) f) . c = (Zmf (C1,C3)) . c ) ; ::_thesis: verum
end;
 dom ((Zmf (C1,C2)) (#) f) = [:C1,C3:] by FUNCT_2:def_1;
hence  (Zmf (C1,C2)) (#) f = Zmf (C1,C3) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

Lm7:  for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z]
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z]
let f be RMembership_Func of C1,C2; ::_thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z]
let x, z be set ; ::_thesis: ( x in C1 & z in C3 implies upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z] )
assume that
A1: x in C1 and
A2: z in C3 ; ::_thesis: upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z]
 rng (min (f,(Zmf (C2,C3)),x,z)) is real-bounded by Th1;
then A3: rng (min (f,(Zmf (C2,C3)),x,z)) is bounded_above by XXREAL_2:def_11;
 for s being real number st 0 < s holds
(upper_bound (rng (min (f,(Zmf (C2,C3)),x,z)))) - s <= (Zmf (C1,C3)) . [x,z]
proof
let s be real number ; ::_thesis: ( 0 < s implies (upper_bound (rng (min (f,(Zmf (C2,C3)),x,z)))) - s <= (Zmf (C1,C3)) . [x,z] )
assume  s > 0 ; ::_thesis: (upper_bound (rng (min (f,(Zmf (C2,C3)),x,z)))) - s <= (Zmf (C1,C3)) . [x,z]
then consider r being real number  such that
A4: r in rng (min (f,(Zmf (C2,C3)),x,z)) and
A5: (upper_bound (rng (min (f,(Zmf (C2,C3)),x,z)))) - s < r by A3, SEQ_4:def_1;
consider y being set  such that
A6: y in dom (min (f,(Zmf (C2,C3)),x,z)) and
A7: r = (min (f,(Zmf (C2,C3)),x,z)) . y by A4, FUNCT_1:def_3;
A8: [y,z] in [:C2,C3:] by A2, A6, ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
A10: 0 <= f . [x,y] by Th3;
r = min ((f . [x,y]),((Zmf (C2,C3)) . [y,z])) by A1, A2, A6, A7, Def2
.= min ((f . [x,y]),0) by A8, FUNCT_3:def_3
.= 0 by A10, XXREAL_0:def_9
.= (Zmf (C1,C3)) . [x,z] by A9, FUNCT_3:def_3 ;
hence  (upper_bound (rng (min (f,(Zmf (C2,C3)),x,z)))) - s <= (Zmf (C1,C3)) . [x,z] by A5; ::_thesis: verum
end;
then A11: upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) <= (Zmf (C1,C3)) . [x,z] by XREAL_1:57;
 upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) >= (Zmf (C1,C3)) . [x,z]
proof
reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
 rng (min (f,(Zmf (C2,C3)),x,z)) c= [.0,1.] by RELAT_1:def_19;
then A13: lower_bound A <= lower_bound (rng (min (f,(Zmf (C2,C3)),x,z))) by A12, SEQ_4:47;
 A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A14: 0 = lower_bound A by INTEGRA1:5;
A15: lower_bound (rng (min (f,(Zmf (C2,C3)),x,z))) <= upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) by Th1, SEQ_4:11;
 [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
hence  upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) >= (Zmf (C1,C3)) . [x,z] by A14, A13, A15, FUNCT_3:def_3; ::_thesis: verum
end;
hence  upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) = (Zmf (C1,C3)) . [x,z] by A11, XXREAL_0:1; ::_thesis: verum
end;

theorem Th23: :: FUZZY_4:23
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2 holds f (#) (Zmf (C2,C3)) = Zmf (C1,C3)
proof
let C1, C2, C3 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2 holds f (#) (Zmf (C2,C3)) = Zmf (C1,C3)
let f be RMembership_Func of C1,C2; ::_thesis: f (#) (Zmf (C2,C3)) = Zmf (C1,C3)
A1: dom (Zmf (C1,C3)) = [:C1,C3:] by FUNCT_2:def_1;
A2: for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
(f (#) (Zmf (C2,C3))) . c = (Zmf (C1,C3)) . c
proof
let c be Element of [:C1,C3:]; ::_thesis: ( c in [:C1,C3:] implies (f (#) (Zmf (C2,C3))) . c = (Zmf (C1,C3)) . c )
consider x, z being set  such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def_2;
(f (#) (Zmf (C2,C3))) . c = (f (#) (Zmf (C2,C3))) . (x,z) by A5
.= upper_bound (rng (min (f,(Zmf (C2,C3)),x,z))) by A5, Def3
.= (Zmf (C1,C3)) . c by A3, A4, A5, Lm7 ;
hence  ( c in [:C1,C3:] implies (f (#) (Zmf (C2,C3))) . c = (Zmf (C1,C3)) . c ) ; ::_thesis: verum
end;
 dom (f (#) (Zmf (C2,C3))) = [:C1,C3:] by FUNCT_2:def_1;
hence  f (#) (Zmf (C2,C3)) = Zmf (C1,C3) by A1, A2, PARTFUN1:5; ::_thesis: verum
end;

theorem :: FUZZY_4:24
for C1 being non empty set
for f being RMembership_Func of C1,C1 holds f (#) (Zmf (C1,C1)) = (Zmf (C1,C1)) (#) f
proof
let C1 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C1 holds f (#) (Zmf (C1,C1)) = (Zmf (C1,C1)) (#) f
let f be RMembership_Func of C1,C1; ::_thesis: f (#) (Zmf (C1,C1)) = (Zmf (C1,C1)) (#) f
 f (#) (Zmf (C1,C1)) = Zmf (C1,C1) by Th23;
hence  f (#) (Zmf (C1,C1)) = (Zmf (C1,C1)) (#) f by Th22; ::_thesis: verum
end;

begin

theorem :: FUZZY_4:25
for X, Y being non empty set
for x being Element of X
for y being Element of Y holds
( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
proof
let X, Y be non empty set ; ::_thesis: for x being Element of X
for y being Element of Y holds
( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
let x be Element of X; ::_thesis: for y being Element of Y holds
( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
let y be Element of Y; ::_thesis: ( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) )
 [x,y] in [:X,Y:] by ZFMISC_1:87;
hence  ( ( x = y implies (Imf (X,Y)) . (x,y) = 1 ) & ( x <> y implies (Imf (X,Y)) . (x,y) = 0 ) ) by Def4; ::_thesis: verum
end;

theorem :: FUZZY_4:26
for X, Y being non empty set
for x being Element of X
for y being Element of Y
for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
proof
let X, Y be non empty set ; ::_thesis: for x being Element of X
for y being Element of Y
for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
let x be Element of X; ::_thesis: for y being Element of Y
for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
let y be Element of Y; ::_thesis: for f being RMembership_Func of X,Y holds (converse f) . (y,x) = f . (x,y)
let f be RMembership_Func of X,Y; ::_thesis: (converse f) . (y,x) = f . (x,y)
 [y,x] in [:Y,X:] by ZFMISC_1:87;
hence  (converse f) . (y,x) = f . (x,y) by Def1; ::_thesis: verum
end;