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