:: FUZZY_1 semantic presentation begin registration let x, y be set ; clusterK146(x,y) -> [.0,1.] -valued ; coherence chi (x,y) is [.0,1.] -valued proof ( 1 in [.0,1.] & 0 in [.0,1.] ) by XXREAL_1:1; then ( rng (chi (x,y)) c= {0,1} & {0,1} c= [.0,1.] ) by FUNCT_3:39, ZFMISC_1:32; hence rng (chi (x,y)) c= [.0,1.] by XBOOLE_1:1; :: according to RELAT_1:def_19 ::_thesis: verum end; end; registration let C be non empty set ; cluster non empty Relation-like C -defined REAL -valued [.0,1.] -valued Function-like total V30(C, REAL ) complex-valued ext-real-valued real-valued for Element of K6(K7(C,REAL)); existence ex b1 being Function of C,REAL st b1 is [.0,1.] -valued proof take chi (C,C) ; ::_thesis: chi (C,C) is [.0,1.] -valued thus rng (chi (C,C)) c= [.0,1.] by RELAT_1:def_19; :: according to RELAT_1:def_19 ::_thesis: verum end; end; definition let C be non empty set ; mode Membership_Func of C is [.0,1.] -valued Function of C,REAL; end; theorem :: FUZZY_1:1 for C being non empty set holds chi (C,C) is Membership_Func of C ; registration let X be non empty set ; cluster[.0,1.] -valued Function-like V30(X, REAL ) -> real-valued for Element of K6(K7(X,REAL)); coherence for b1 being Membership_Func of X holds b1 is real-valued ; end; definition let f, g be real-valued Function; predf is_less_than g means :Def1: :: FUZZY_1:def 1 ( dom f c= dom g & ( for x being set st x in dom f holds f . x <= g . x ) ); reflexivity for f being real-valued Function holds ( dom f c= dom f & ( for x being set st x in dom f holds f . x <= f . x ) ) ; end; :: deftheorem Def1 defines is_less_than FUZZY_1:def_1_:_ for f, g being real-valued Function holds ( f is_less_than g iff ( dom f c= dom g & ( for x being set st x in dom f holds f . x <= g . x ) ) ); notation let X be non empty set ; let f, g be Membership_Func of X; synonym f c= g for X is_less_than f; end; definition let X be non empty set ; let f, g be Membership_Func of X; :: original: is_less_than redefine predf is_less_than g means :Def2: :: FUZZY_1:def 2 for x being Element of X holds f . x <= g . x; compatibility ( f is_less_than g iff for x being Element of X holds f . x <= g . x ) proof thus ( f is_less_than g iff for x being Element of X holds f . x <= g . x ) ::_thesis: verum proof hereby ::_thesis: ( ( for x being Element of X holds f . x <= g . x ) implies f is_less_than g ) assume A1: f is_less_than g ; ::_thesis: for x being Element of X holds f . x <= g . x thus for x being Element of X holds f . x <= g . x ::_thesis: verum proof let x be Element of X; ::_thesis: f . x <= g . x dom f = X by FUNCT_2:def_1; hence f . x <= g . x by A1, Def1; ::_thesis: verum end; end; assume for x being Element of X holds f . x <= g . x ; ::_thesis: f is_less_than g then ( dom g = X & ( for x being set st x in dom f holds f . x <= g . x ) ) by FUNCT_2:def_1; hence f is_less_than g by Def1; ::_thesis: verum end; end; end; :: deftheorem Def2 defines is_less_than FUZZY_1:def_2_:_ for X being non empty set for f, g being Membership_Func of X holds ( f is_less_than g iff for x being Element of X holds f . x <= g . x ); Lm1: for C being non empty set for f, g being Membership_Func of C st g c= & f c= holds f = g proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= & f c= holds f = g let f, g be Membership_Func of C; ::_thesis: ( g c= & f c= implies f = g ) set A = f; set B = g; assume A1: ( g c= & f c= ) ; ::_thesis: f = g A2: for c being Element of C st c in C holds f . c = g . c proof let c be Element of C; ::_thesis: ( c in C implies f . c = g . c ) ( f . c <= g . c & g . c <= f . c ) by A1, Def2; hence ( c in C implies f . c = g . c ) by XXREAL_0:1; ::_thesis: verum end; ( C = dom f & C = dom g ) by FUNCT_2:def_1; hence f = g by A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_1:2 for C being non empty set for f, g being Membership_Func of C holds ( f = g iff ( g c= & f c= ) ) by Lm1; theorem :: FUZZY_1:3 for C being non empty set for f being Membership_Func of C holds f c= ; theorem :: FUZZY_1:4 for C being non empty set for f, g, h being Membership_Func of C st g c= & h c= holds h c= ; begin definition let C be non empty set ; let h, g be Membership_Func of C; func min (h,g) -> Membership_Func of C means :Def3: :: FUZZY_1:def 3 for c being Element of C holds it . c = min ((h . c),(g . c)); existence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = min ((h . c),(g . c)) proof defpred S1[ set , set ] means \$2 = min ((h . \$1),(g . \$1)); A1: for x, y1, y2 being set st x in C & S1[x,y1] & S1[x,y2] holds y1 = y2 ; A2: for x, y being set st x in C & S1[x,y] holds y in REAL ; consider IT being PartFunc of C,REAL such that A3: ( ( for x being set holds ( x in dom IT iff ( x in C & ex y being set st S1[x,y] ) ) ) & ( for x being set st x in dom IT holds S1[x,IT . x] ) ) from PARTFUN1:sch_2(A2, A1); for x being set st x in C holds x in dom IT proof let x be set ; ::_thesis: ( x in C implies x in dom IT ) A4: ex y being set st y = min ((h . x),(g . x)) ; assume x in C ; ::_thesis: x in dom IT hence x in dom IT by A3, A4; ::_thesis: verum end; then C c= dom IT by TARSKI:def_3; then A5: dom IT = C by XBOOLE_0:def_10; then A6: for c being Element of C holds IT . c = min ((h . c),(g . c)) by A3; A7: rng h c= [.0,1.] by RELAT_1:def_19; A8: rng g c= [.0,1.] by RELAT_1:def_19; for y being set st y in rng IT holds y in [.0,1.] proof reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] ) assume y in rng IT ; ::_thesis: y in [.0,1.] then consider x being Element of C such that A9: x in dom IT and A10: y = IT . x by PARTFUN1:3; A11: h . x >= min ((h . x),(g . x)) by XXREAL_0:17; A12: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A13: 0 = lower_bound A by INTEGRA1:5; A14: x in C ; then x in dom h by FUNCT_2:def_1; then A15: h . x in rng h by FUNCT_1:def_3; A16: 1 = upper_bound A by A12, INTEGRA1:5; then h . x <= 1 by A7, A15, INTEGRA2:1; then min ((h . x),(g . x)) <= 1 by A11, XXREAL_0:2; then A17: IT . x <= 1 by A3, A9; x in dom g by A14, FUNCT_2:def_1; then g . x in rng g by FUNCT_1:def_3; then A18: 0 <= g . x by A8, A13, INTEGRA2:1; 0 <= h . x by A7, A13, A15, INTEGRA2:1; then 0 <= min ((h . x),(g . x)) by A18, XXREAL_0:20; then 0 <= IT . x by A3, A9; hence y in [.0,1.] by A10, A13, A16, A17, INTEGRA2:1; ::_thesis: verum end; then A19: rng IT c= [.0,1.] by TARSKI:def_3; IT is total by A5, PARTFUN1:def_2; then IT is Membership_Func of C by A19, RELAT_1:def_19; hence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = min ((h . c),(g . c)) by A6; ::_thesis: verum end; uniqueness for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = min ((h . c),(g . c)) ) holds b1 = b2 proof let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = min ((h . c),(g . c)) ) & ( for c being Element of C holds G . c = min ((h . c),(g . c)) ) implies F = G ) assume that A20: for c being Element of C holds F . c = min ((h . c),(g . c)) and A21: for c being Element of C holds G . c = min ((h . c),(g . c)) ; ::_thesis: F = G A22: for c being Element of C st c in C holds F . c = G . c proof let c be Element of C; ::_thesis: ( c in C implies F . c = G . c ) F . c = min ((h . c),(g . c)) by A20; hence ( c in C implies F . c = G . c ) by A21; ::_thesis: verum end; ( C = dom F & C = dom G ) by FUNCT_2:def_1; hence F = G by A22, PARTFUN1:5; ::_thesis: verum end; idempotence for h being Membership_Func of C for c being Element of C holds h . c = min ((h . c),(h . c)) ; commutativity for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = min ((h . c),(g . c)) ) holds for c being Element of C holds b1 . c = min ((g . c),(h . c)) ; end; :: deftheorem Def3 defines min FUZZY_1:def_3_:_ for C being non empty set for h, g, b4 being Membership_Func of C holds ( b4 = min (h,g) iff for c being Element of C holds b4 . c = min ((h . c),(g . c)) ); definition let C be non empty set ; let h, g be Membership_Func of C; func max (h,g) -> Membership_Func of C means :Def4: :: FUZZY_1:def 4 for c being Element of C holds it . c = max ((h . c),(g . c)); existence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = max ((h . c),(g . c)) proof defpred S1[ set , set ] means \$2 = max ((h . \$1),(g . \$1)); A1: for x, y1, y2 being set st x in C & S1[x,y1] & S1[x,y2] holds y1 = y2 ; A2: for x, y being set st x in C & S1[x,y] holds y in REAL ; consider IT being PartFunc of C,REAL such that A3: ( ( for x being set holds ( x in dom IT iff ( x in C & ex y being set st S1[x,y] ) ) ) & ( for x being set st x in dom IT holds S1[x,IT . x] ) ) from PARTFUN1:sch_2(A2, A1); for x being set st x in C holds x in dom IT proof let x be set ; ::_thesis: ( x in C implies x in dom IT ) A4: ex y being set st y = max ((h . x),(g . x)) ; assume x in C ; ::_thesis: x in dom IT hence x in dom IT by A3, A4; ::_thesis: verum end; then C c= dom IT by TARSKI:def_3; then A5: dom IT = C by XBOOLE_0:def_10; then A6: for c being Element of C holds IT . c = max ((h . c),(g . c)) by A3; A7: rng h c= [.0,1.] by RELAT_1:def_19; A8: rng g c= [.0,1.] by RELAT_1:def_19; for y being set st y in rng IT holds y in [.0,1.] proof reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] ) assume y in rng IT ; ::_thesis: y in [.0,1.] then consider x being Element of C such that A9: x in dom IT and A10: y = IT . x by PARTFUN1:3; A11: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A12: 0 = lower_bound A by INTEGRA1:5; A13: x in C ; then x in dom h by FUNCT_2:def_1; then A14: h . x in rng h by FUNCT_1:def_3; then 0 <= h . x by A7, A12, INTEGRA2:1; then 0 <= max ((h . x),(g . x)) by XXREAL_0:30; then A15: 0 <= IT . x by A3, A9; A16: 1 = upper_bound A by A11, INTEGRA1:5; x in dom g by A13, FUNCT_2:def_1; then g . x in rng g by FUNCT_1:def_3; then A17: g . x <= 1 by A8, A16, INTEGRA2:1; h . x <= 1 by A7, A16, A14, INTEGRA2:1; then max ((h . x),(g . x)) <= 1 by A17, XXREAL_0:28; then IT . x <= 1 by A3, A9; hence y in [.0,1.] by A10, A12, A16, A15, INTEGRA2:1; ::_thesis: verum end; then A18: rng IT c= [.0,1.] by TARSKI:def_3; IT is total by A5, PARTFUN1:def_2; then IT is Membership_Func of C by A18, RELAT_1:def_19; hence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = max ((h . c),(g . c)) by A6; ::_thesis: verum end; uniqueness for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) & ( for c being Element of C holds b2 . c = max ((h . c),(g . c)) ) holds b1 = b2 proof let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = max ((h . c),(g . c)) ) & ( for c being Element of C holds G . c = max ((h . c),(g . c)) ) implies F = G ) assume that A19: for c being Element of C holds F . c = max ((h . c),(g . c)) and A20: for c being Element of C holds G . c = max ((h . c),(g . c)) ; ::_thesis: F = G A21: for c being Element of C st c in C holds F . c = G . c proof let c be Element of C; ::_thesis: ( c in C implies F . c = G . c ) F . c = max ((h . c),(g . c)) by A19; hence ( c in C implies F . c = G . c ) by A20; ::_thesis: verum end; ( C = dom F & C = dom G ) by FUNCT_2:def_1; hence F = G by A21, PARTFUN1:5; ::_thesis: verum end; idempotence for h being Membership_Func of C for c being Element of C holds h . c = max ((h . c),(h . c)) ; commutativity for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = max ((h . c),(g . c)) ) holds for c being Element of C holds b1 . c = max ((g . c),(h . c)) ; end; :: deftheorem Def4 defines max FUZZY_1:def_4_:_ for C being non empty set for h, g, b4 being Membership_Func of C holds ( b4 = max (h,g) iff for c being Element of C holds b4 . c = max ((h . c),(g . c)) ); definition let C be non empty set ; let h be Membership_Func of C; func 1_minus h -> Membership_Func of C means :Def5: :: FUZZY_1:def 5 for c being Element of C holds it . c = 1 - (h . c); existence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = 1 - (h . c) proof deffunc H1( set ) -> Element of REAL = 1 - (h . \$1); defpred S1[ set ] means \$1 in dom h; consider IT being PartFunc of C,REAL such that A1: ( ( for x being Element of C holds ( x in dom IT iff S1[x] ) ) & ( for x being Element of C st x in dom IT holds IT . x = H1(x) ) ) from SEQ_1:sch_3(); for x being set st x in C holds x in dom IT proof let x be set ; ::_thesis: ( x in C implies x in dom IT ) A2: dom h = C by FUNCT_2:def_1; assume x in C ; ::_thesis: x in dom IT hence x in dom IT by A1, A2; ::_thesis: verum end; then C c= dom IT by TARSKI:def_3; then A3: dom IT = C by XBOOLE_0:def_10; then A4: for c being Element of C holds IT . c = 1 - (h . c) by A1; A5: rng h c= [.0,1.] by RELAT_1:def_19; for y being set st y in rng IT holds y in [.0,1.] proof reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] ) assume y in rng IT ; ::_thesis: y in [.0,1.] then consider x being Element of C such that A6: x in dom IT and A7: y = IT . x by PARTFUN1:3; A8: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A9: 0 = lower_bound A by INTEGRA1:5; x in C ; then x in dom h by FUNCT_2:def_1; then A10: h . x in rng h by FUNCT_1:def_3; then 0 <= h . x by A5, A9, INTEGRA2:1; then 0 + 1 <= 1 + (h . x) by XREAL_1:6; then 1 - (h . x) <= 1 by XREAL_1:20; then A11: IT . x <= 1 by A1, A6; A12: 1 = upper_bound A by A8, INTEGRA1:5; then h . x <= 1 by A5, A10, INTEGRA2:1; then 0 <= 1 - (h . x) by XREAL_1:48; then 0 <= IT . x by A1, A6; hence y in [.0,1.] by A7, A9, A12, A11, INTEGRA2:1; ::_thesis: verum end; then A13: rng IT c= [.0,1.] by TARSKI:def_3; IT is total by A3, PARTFUN1:def_2; then IT is Membership_Func of C by A13, RELAT_1:def_19; hence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = 1 - (h . c) by A4; ::_thesis: verum end; uniqueness for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (h . c) ) & ( for c being Element of C holds b2 . c = 1 - (h . c) ) holds b1 = b2 proof let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = 1 - (h . c) ) & ( for c being Element of C holds G . c = 1 - (h . c) ) implies F = G ) assume that A14: for c being Element of C holds F . c = 1 - (h . c) and A15: for c being Element of C holds G . c = 1 - (h . c) ; ::_thesis: F = G A16: for c being Element of C st c in C holds F . c = G . c proof let c be Element of C; ::_thesis: ( c in C implies F . c = G . c ) F . c = 1 - (h . c) by A14; hence ( c in C implies F . c = G . c ) by A15; ::_thesis: verum end; ( C = dom F & C = dom G ) by FUNCT_2:def_1; hence F = G by A16, PARTFUN1:5; ::_thesis: verum end; involutiveness for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = 1 - (b2 . c) ) holds for c being Element of C holds b2 . c = 1 - (b1 . c) proof let h1, h2 be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds h1 . c = 1 - (h2 . c) ) implies for c being Element of C holds h2 . c = 1 - (h1 . c) ) assume A17: for c being Element of C holds h1 . c = 1 - (h2 . c) ; ::_thesis: for c being Element of C holds h2 . c = 1 - (h1 . c) let c be Element of C; ::_thesis: h2 . c = 1 - (h1 . c) thus h2 . c = 1 - (1 - (h2 . c)) .= 1 - (h1 . c) by A17 ; ::_thesis: verum end; end; :: deftheorem Def5 defines 1_minus FUZZY_1:def_5_:_ for C being non empty set for h, b3 being Membership_Func of C holds ( b3 = 1_minus h iff for c being Element of C holds b3 . c = 1 - (h . c) ); theorem :: FUZZY_1:5 for C being non empty set for c being Element of C for h, g being Membership_Func of C holds ( min ((h . c),(g . c)) = (min (h,g)) . c & max ((h . c),(g . c)) = (max (h,g)) . c ) by Def3, Def4; theorem :: FUZZY_1:6 for C being non empty set for h, f, g being Membership_Func of C holds ( max (h,h) = h & min (h,h) = h & max (h,h) = min (h,h) & min (f,g) = min (g,f) & max (f,g) = max (g,f) ) ; theorem Th7: :: FUZZY_1:7 for C being non empty set for f, g, h being Membership_Func of C holds ( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) ) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds ( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) ) let f, g, h be Membership_Func of C; ::_thesis: ( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) ) A1: ( C = dom (min ((min (f,g)),h)) & C = dom (min (f,(min (g,h)))) ) by FUNCT_2:def_1; A2: for x being Element of C st x in C holds (max ((max (f,g)),h)) . x = (max (f,(max (g,h)))) . x proof let x be Element of C; ::_thesis: ( x in C implies (max ((max (f,g)),h)) . x = (max (f,(max (g,h)))) . x ) (max ((max (f,g)),h)) . x = max (((max (f,g)) . x),(h . x)) by Def4 .= max ((max ((f . x),(g . x))),(h . x)) by Def4 .= max ((f . x),(max ((g . x),(h . x)))) by XXREAL_0:34 .= max ((f . x),((max (g,h)) . x)) by Def4 .= (max (f,(max (g,h)))) . x by Def4 ; hence ( x in C implies (max ((max (f,g)),h)) . x = (max (f,(max (g,h)))) . x ) ; ::_thesis: verum end; A3: for x being Element of C st x in C holds (min ((min (f,g)),h)) . x = (min (f,(min (g,h)))) . x proof let x be Element of C; ::_thesis: ( x in C implies (min ((min (f,g)),h)) . x = (min (f,(min (g,h)))) . x ) (min ((min (f,g)),h)) . x = min (((min (f,g)) . x),(h . x)) by Def3 .= min ((min ((f . x),(g . x))),(h . x)) by Def3 .= min ((f . x),(min ((g . x),(h . x)))) by XXREAL_0:33 .= min ((f . x),((min (g,h)) . x)) by Def3 .= (min (f,(min (g,h)))) . x by Def3 ; hence ( x in C implies (min ((min (f,g)),h)) . x = (min (f,(min (g,h)))) . x ) ; ::_thesis: verum end; ( C = dom (max ((max (f,g)),h)) & C = dom (max (f,(max (g,h)))) ) by FUNCT_2:def_1; hence ( max ((max (f,g)),h) = max (f,(max (g,h))) & min ((min (f,g)),h) = min (f,(min (g,h))) ) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th8: :: FUZZY_1:8 for C being non empty set for f, g being Membership_Func of C holds ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f ) let f, g be Membership_Func of C; ::_thesis: ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f ) A1: C = dom (min (f,(max (f,g)))) by FUNCT_2:def_1; A2: for x being Element of C st x in C holds (max (f,(min (f,g)))) . x = f . x proof let x be Element of C; ::_thesis: ( x in C implies (max (f,(min (f,g)))) . x = f . x ) (max (f,(min (f,g)))) . x = max ((f . x),((min (f,g)) . x)) by Def4 .= max ((f . x),(min ((f . x),(g . x)))) by Def3 .= f . x by XXREAL_0:36 ; hence ( x in C implies (max (f,(min (f,g)))) . x = f . x ) ; ::_thesis: verum end; A3: for x being Element of C st x in C holds (min (f,(max (f,g)))) . x = f . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,(max (f,g)))) . x = f . x ) (min (f,(max (f,g)))) . x = min ((f . x),((max (f,g)) . x)) by Def3 .= min ((f . x),(max ((f . x),(g . x)))) by Def4 .= f . x by XXREAL_0:35 ; hence ( x in C implies (min (f,(max (f,g)))) . x = f . x ) ; ::_thesis: verum end; ( C = dom (max (f,(min (f,g)))) & C = dom f ) by FUNCT_2:def_1; hence ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f ) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th9: :: FUZZY_1:9 for C being non empty set for f, g, h being Membership_Func of C holds ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) ) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) ) let f, g, h be Membership_Func of C; ::_thesis: ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) ) A1: ( C = dom (max (f,(min (g,h)))) & C = dom (min ((max (f,g)),(max (f,h)))) ) by FUNCT_2:def_1; A2: for x being Element of C st x in C holds (min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x ) (min (f,(max (g,h)))) . x = min ((f . x),((max (g,h)) . x)) by Def3 .= min ((f . x),(max ((g . x),(h . x)))) by Def4 .= max ((min ((f . x),(g . x))),(min ((f . x),(h . x)))) by XXREAL_0:38 .= max (((min (f,g)) . x),(min ((f . x),(h . x)))) by Def3 .= max (((min (f,g)) . x),((min (f,h)) . x)) by Def3 .= (max ((min (f,g)),(min (f,h)))) . x by Def4 ; hence ( x in C implies (min (f,(max (g,h)))) . x = (max ((min (f,g)),(min (f,h)))) . x ) ; ::_thesis: verum end; A3: for x being Element of C st x in C holds (max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x proof let x be Element of C; ::_thesis: ( x in C implies (max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x ) (max (f,(min (g,h)))) . x = max ((f . x),((min (g,h)) . x)) by Def4 .= max ((f . x),(min ((g . x),(h . x)))) by Def3 .= min ((max ((f . x),(g . x))),(max ((f . x),(h . x)))) by XXREAL_0:39 .= min (((max (f,g)) . x),(max ((f . x),(h . x)))) by Def4 .= min (((max (f,g)) . x),((max (f,h)) . x)) by Def4 .= (min ((max (f,g)),(max (f,h)))) . x by Def3 ; hence ( x in C implies (max (f,(min (g,h)))) . x = (min ((max (f,g)),(max (f,h)))) . x ) ; ::_thesis: verum end; ( C = dom (min (f,(max (g,h)))) & C = dom (max ((min (f,g)),(min (f,h)))) ) by FUNCT_2:def_1; hence ( min (f,(max (g,h))) = max ((min (f,g)),(min (f,h))) & max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) ) by A1, A2, A3, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_1:10 canceled; theorem Th11: :: FUZZY_1:11 for C being non empty set for f, g being Membership_Func of C holds ( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) ) let f, g be Membership_Func of C; ::_thesis: ( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) ) A1: ( C = dom (1_minus (min (f,g))) & C = dom (max ((1_minus f),(1_minus g))) ) by FUNCT_2:def_1; A2: for x being Element of C st x in C holds (1_minus (max (f,g))) . x = (min ((1_minus f),(1_minus g))) . x proof let x be Element of C; ::_thesis: ( x in C implies (1_minus (max (f,g))) . x = (min ((1_minus f),(1_minus g))) . x ) A3: (1_minus (max (f,g))) . x = 1 - ((max (f,g)) . x) by Def5 .= 1 - (max ((f . x),(g . x))) by Def4 .= 1 - ((((f . x) + (g . x)) + (abs ((f . x) - (g . x)))) / 2) by COMPLEX1:74 ; (min ((1_minus f),(1_minus g))) . x = min (((1_minus f) . x),((1_minus g) . x)) by Def3 .= min ((1 - (f . x)),((1_minus g) . x)) by Def5 .= min ((1 - (f . x)),(1 - (g . x))) by Def5 .= (((1 - (f . x)) + (1 - (g . x))) - (abs ((1 - (f . x)) - (1 - (g . x))))) / 2 by COMPLEX1:73 .= (((2 - (f . x)) - (g . x)) - (abs (- ((f . x) - (g . x))))) / 2 .= ((2 - ((f . x) + (g . x))) - (abs ((f . x) - (g . x)))) / 2 by COMPLEX1:52 .= 1 - ((((f . x) + (g . x)) + (abs ((f . x) - (g . x)))) / 2) ; hence ( x in C implies (1_minus (max (f,g))) . x = (min ((1_minus f),(1_minus g))) . x ) by A3; ::_thesis: verum end; A4: for x being Element of C st x in C holds (1_minus (min (f,g))) . x = (max ((1_minus f),(1_minus g))) . x proof let x be Element of C; ::_thesis: ( x in C implies (1_minus (min (f,g))) . x = (max ((1_minus f),(1_minus g))) . x ) A5: (1_minus (min (f,g))) . x = 1 - ((min (f,g)) . x) by Def5 .= 1 - (min ((f . x),(g . x))) by Def3 .= 1 - ((((f . x) + (g . x)) - (abs ((f . x) - (g . x)))) / 2) by COMPLEX1:73 ; (max ((1_minus f),(1_minus g))) . x = max (((1_minus f) . x),((1_minus g) . x)) by Def4 .= max ((1 - (f . x)),((1_minus g) . x)) by Def5 .= max ((1 - (f . x)),(1 - (g . x))) by Def5 .= (((1 - (f . x)) + (1 - (g . x))) + (abs ((1 - (f . x)) - (1 - (g . x))))) / 2 by COMPLEX1:74 .= (((2 - (f . x)) - (g . x)) + (abs (- ((f . x) - (g . x))))) / 2 .= ((2 - ((f . x) + (g . x))) + (abs ((f . x) - (g . x)))) / 2 by COMPLEX1:52 .= 1 - ((((f . x) + (g . x)) - (abs ((f . x) - (g . x)))) / 2) ; hence ( x in C implies (1_minus (min (f,g))) . x = (max ((1_minus f),(1_minus g))) . x ) by A5; ::_thesis: verum end; ( C = dom (1_minus (max (f,g))) & C = dom (min ((1_minus f),(1_minus g))) ) by FUNCT_2:def_1; hence ( 1_minus (max (f,g)) = min ((1_minus f),(1_minus g)) & 1_minus (min (f,g)) = max ((1_minus f),(1_minus g)) ) by A1, A2, A4, PARTFUN1:5; ::_thesis: verum end; begin theorem :: FUZZY_1:12 for C being non empty set holds chi ({},C) is Membership_Func of C ; definition let C be non empty set ; func EMF C -> Membership_Func of C equals :: FUZZY_1:def 6 chi ({},C); correctness coherence chi ({},C) is Membership_Func of C; ; end; :: deftheorem defines EMF FUZZY_1:def_6_:_ for C being non empty set holds EMF C = chi ({},C); definition let C be non empty set ; func UMF C -> Membership_Func of C equals :: FUZZY_1:def 7 chi (C,C); correctness coherence chi (C,C) is Membership_Func of C; ; end; :: deftheorem defines UMF FUZZY_1:def_7_:_ for C being non empty set holds UMF C = chi (C,C); theorem Th13: :: FUZZY_1:13 for C being non empty set for a, b being Element of REAL for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) proof let C be non empty set ; ::_thesis: for a, b being Element of REAL for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) let a, b be Element of REAL ; ::_thesis: for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) let f be PartFunc of C,REAL; ::_thesis: ( rng f c= [.a,b.] & a <= b implies for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) ) assume that A1: rng f c= [.a,b.] and A2: a <= b ; ::_thesis: for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) proof reconsider A = [.a,b.] as non empty closed_interval Subset of REAL by A2, MEASURE5:14; let x be Element of C; ::_thesis: ( x in dom f implies ( a <= f . x & f . x <= b ) ) A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A3: ( a = lower_bound A & b = upper_bound A ) by INTEGRA1:5; assume x in dom f ; ::_thesis: ( a <= f . x & f . x <= b ) then f . x in rng f by FUNCT_1:def_3; hence ( a <= f . x & f . x <= b ) by A1, A3, INTEGRA2:1; ::_thesis: verum end; hence for x being Element of C st x in dom f holds ( a <= f . x & f . x <= b ) ; ::_thesis: verum end; theorem Th14: :: FUZZY_1:14 for C being non empty set for f being Membership_Func of C holds f c= proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds f c= let f be Membership_Func of C; ::_thesis: f c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (EMF C) . x <= f . x A1: rng f c= [.0,1.] by RELAT_1:def_19; ( dom f = C & (EMF C) . x = 0 ) by FUNCT_2:def_1, FUNCT_3:def_3; hence (EMF C) . x <= f . x by A1, Th13; ::_thesis: verum end; theorem Th15: :: FUZZY_1:15 for C being non empty set for f being Membership_Func of C holds UMF C c= proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds UMF C c= let f be Membership_Func of C; ::_thesis: UMF C c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (UMF C) . x A1: rng f c= [.0,1.] by RELAT_1:def_19; ( dom f = C & (UMF C) . x = 1 ) by FUNCT_2:def_1, FUNCT_3:def_3; hence f . x <= (UMF C) . x by A1, Th13; ::_thesis: verum end; theorem Th16: :: FUZZY_1:16 for C being non empty set for x being Element of C for h being Membership_Func of C holds ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) proof let C be non empty set ; ::_thesis: for x being Element of C for h being Membership_Func of C holds ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) let x be Element of C; ::_thesis: for h being Membership_Func of C holds ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) let h be Membership_Func of C; ::_thesis: ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) ( h c= & UMF C c= ) by Th14, Th15; hence ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) by Def2; ::_thesis: verum end; theorem Th17: :: FUZZY_1:17 for C being non empty set for f, g being Membership_Func of C holds ( f c= & max (f,g) c= ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( f c= & max (f,g) c= ) let f, g be Membership_Func of C; ::_thesis: ( f c= & max (f,g) c= ) thus f c= ::_thesis: max (f,g) c= proof let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,g)) . x <= f . x (min (f,g)) . x = min ((f . x),(g . x)) by Def3; hence (min (f,g)) . x <= f . x by XXREAL_0:17; ::_thesis: verum end; let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (max (f,g)) . x (max (f,g)) . x = max ((f . x),(g . x)) by Def4; hence f . x <= (max (f,g)) . x by XXREAL_0:25; ::_thesis: verum end; theorem Th18: :: FUZZY_1:18 for C being non empty set for f being Membership_Func of C holds ( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds ( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) let f be Membership_Func of C; ::_thesis: ( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) A1: ( C = dom (max (f,(EMF C))) & C = dom (min (f,(EMF C))) ) by FUNCT_2:def_1; A2: for x being Element of C st x in C holds (min (f,(UMF C))) . x = f . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,(UMF C))) . x = f . x ) A3: f . x <= (UMF C) . x by Th16; (min (f,(UMF C))) . x = min ((f . x),((UMF C) . x)) by Def3 .= f . x by A3, XXREAL_0:def_9 ; hence ( x in C implies (min (f,(UMF C))) . x = f . x ) ; ::_thesis: verum end; A4: for x being Element of C st x in C holds (min (f,(EMF C))) . x = (EMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x ) A5: (EMF C) . x <= f . x by Th16; (min (f,(EMF C))) . x = min ((f . x),((EMF C) . x)) by Def3 .= (EMF C) . x by A5, XXREAL_0:def_9 ; hence ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x ) ; ::_thesis: verum end; A6: for x being Element of C st x in C holds (max (f,(EMF C))) . x = f . x proof let x be Element of C; ::_thesis: ( x in C implies (max (f,(EMF C))) . x = f . x ) A7: (EMF C) . x <= f . x by Th16; (max (f,(EMF C))) . x = max ((f . x),((EMF C) . x)) by Def4 .= f . x by A7, XXREAL_0:def_10 ; hence ( x in C implies (max (f,(EMF C))) . x = f . x ) ; ::_thesis: verum end; ( UMF C c= & max (f,(UMF C)) c= ) by Th15, Th17; hence max (f,(UMF C)) = UMF C by Lm1; ::_thesis: ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) A8: C = dom (EMF C) by FUNCT_2:def_1; ( C = dom (min (f,(UMF C))) & C = dom f ) by FUNCT_2:def_1; hence ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) by A2, A6, A1, A8, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th19: :: FUZZY_1:19 for C being non empty set for f, h, g being Membership_Func of C st h c= & h c= holds h c= proof let C be non empty set ; ::_thesis: for f, h, g being Membership_Func of C st h c= & h c= holds h c= let f, h, g be Membership_Func of C; ::_thesis: ( h c= & h c= implies h c= ) assume A1: ( h c= & h c= ) ; ::_thesis: h c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,g)) . x <= h . x A2: max ((f . x),(g . x)) = (max (f,g)) . x by Def4; ( f . x <= h . x & g . x <= h . x ) by A1, Def2; hence (max (f,g)) . x <= h . x by A2, XXREAL_0:28; ::_thesis: verum end; theorem :: FUZZY_1:20 for C being non empty set for f, g, h being Membership_Func of C st g c= holds max (g,h) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= holds max (g,h) c= let f, g, h be Membership_Func of C; ::_thesis: ( g c= implies max (g,h) c= ) assume A1: g c= ; ::_thesis: max (g,h) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,h)) . x <= (max (g,h)) . x f . x <= g . x by A1, Def2; then max ((f . x),(h . x)) <= max ((g . x),(h . x)) by XXREAL_0:26; then max ((f . x),(h . x)) <= (max (g,h)) . x by Def4; hence (max (f,h)) . x <= (max (g,h)) . x by Def4; ::_thesis: verum end; theorem :: FUZZY_1:21 for C being non empty set for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds max (g,h1) c= proof let C be non empty set ; ::_thesis: for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds max (g,h1) c= let f, g, h, h1 be Membership_Func of C; ::_thesis: ( g c= & h1 c= implies max (g,h1) c= ) assume A1: ( g c= & h1 c= ) ; ::_thesis: max (g,h1) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,h)) . x <= (max (g,h1)) . x ( f . x <= g . x & h . x <= h1 . x ) by A1, Def2; then max ((f . x),(h . x)) <= max ((g . x),(h1 . x)) by XXREAL_0:26; then (max (f,h)) . x <= max ((g . x),(h1 . x)) by Def4; hence (max (f,h)) . x <= (max (g,h1)) . x by Def4; ::_thesis: verum end; theorem :: FUZZY_1:22 for C being non empty set for f, g being Membership_Func of C st g c= holds max (f,g) = g proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds max (f,g) = g let f, g be Membership_Func of C; ::_thesis: ( g c= implies max (f,g) = g ) assume g c= ; ::_thesis: max (f,g) = g then A1: g c= by Th19; max (f,g) c= by Th17; hence max (f,g) = g by A1, Lm1; ::_thesis: verum end; theorem :: FUZZY_1:23 for C being non empty set for f, g being Membership_Func of C holds max (f,g) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds max (f,g) c= let f, g be Membership_Func of C; ::_thesis: max (f,g) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,g)) . x <= (max (f,g)) . x ( min ((f . x),(g . x)) <= f . x & f . x <= max ((f . x),(g . x)) ) by XXREAL_0:17, XXREAL_0:25; then min ((f . x),(g . x)) <= max ((f . x),(g . x)) by XXREAL_0:2; then min ((f . x),(g . x)) <= (max (f,g)) . x by Def4; hence (min (f,g)) . x <= (max (f,g)) . x by Def3; ::_thesis: verum end; theorem Th24: :: FUZZY_1:24 for C being non empty set for h, f, g being Membership_Func of C st f c= & g c= holds min (f,g) c= proof let C be non empty set ; ::_thesis: for h, f, g being Membership_Func of C st f c= & g c= holds min (f,g) c= let h, f, g be Membership_Func of C; ::_thesis: ( f c= & g c= implies min (f,g) c= ) assume A1: ( f c= & g c= ) ; ::_thesis: min (f,g) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: h . x <= (min (f,g)) . x ( h . x <= f . x & h . x <= g . x ) by A1, Def2; then h . x <= min ((f . x),(g . x)) by XXREAL_0:20; hence h . x <= (min (f,g)) . x by Def3; ::_thesis: verum end; theorem :: FUZZY_1:25 for C being non empty set for f, g, h being Membership_Func of C st g c= holds min (g,h) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= holds min (g,h) c= let f, g, h be Membership_Func of C; ::_thesis: ( g c= implies min (g,h) c= ) assume A1: g c= ; ::_thesis: min (g,h) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,h)) . x <= (min (g,h)) . x f . x <= g . x by A1, Def2; then min ((f . x),(h . x)) <= min ((g . x),(h . x)) by XXREAL_0:18; then (min (f,h)) . x <= min ((g . x),(h . x)) by Def3; hence (min (f,h)) . x <= (min (g,h)) . x by Def3; ::_thesis: verum end; theorem :: FUZZY_1:26 for C being non empty set for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds min (g,h1) c= proof let C be non empty set ; ::_thesis: for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds min (g,h1) c= let f, g, h, h1 be Membership_Func of C; ::_thesis: ( g c= & h1 c= implies min (g,h1) c= ) assume A1: ( g c= & h1 c= ) ; ::_thesis: min (g,h1) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,h)) . x <= (min (g,h1)) . x ( f . x <= g . x & h . x <= h1 . x ) by A1, Def2; then min ((f . x),(h . x)) <= min ((g . x),(h1 . x)) by XXREAL_0:18; then (min (f,h)) . x <= min ((g . x),(h1 . x)) by Def3; hence (min (f,h)) . x <= (min (g,h1)) . x by Def3; ::_thesis: verum end; theorem Th27: :: FUZZY_1:27 for C being non empty set for f, g being Membership_Func of C st g c= holds min (f,g) = f proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds min (f,g) = f let f, g be Membership_Func of C; ::_thesis: ( g c= implies min (f,g) = f ) assume A1: g c= ; ::_thesis: min (f,g) = f A2: for x being Element of C st x in C holds (min (f,g)) . x = f . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,g)) . x = f . x ) f . x <= g . x by A1, Def2; then f . x = min ((f . x),(g . x)) by XXREAL_0:def_9 .= (min (f,g)) . x by Def3 ; hence ( x in C implies (min (f,g)) . x = f . x ) ; ::_thesis: verum end; ( C = dom (min (f,g)) & C = dom f ) by FUNCT_2:def_1; hence min (f,g) = f by A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_1:28 for C being non empty set for f, g, h being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds f = EMF C proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds f = EMF C let f, g, h be Membership_Func of C; ::_thesis: ( g c= & h c= & min (g,h) = EMF C implies f = EMF C ) assume that A1: ( g c= & h c= ) and A2: min (g,h) = EMF C ; ::_thesis: f = EMF C A3: for x being Element of C st x in C holds f . x = (EMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies f . x = (EMF C) . x ) ( f . x <= g . x & f . x <= h . x ) by A1, Def2; then f . x <= min ((g . x),(h . x)) by XXREAL_0:20; then A4: f . x <= (min (g,h)) . x by Def3; (EMF C) . x <= f . x by Th16; hence ( x in C implies f . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; ::_thesis: verum end; ( C = dom f & C = dom (EMF C) ) by FUNCT_2:def_1; hence f = EMF C by A3, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_1:29 for C being non empty set for f, g, h being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds max (g,h) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds max (g,h) c= let f, g, h be Membership_Func of C; ::_thesis: ( max ((min (f,g)),(min (f,h))) = f implies max (g,h) c= ) assume A1: max ((min (f,g)),(min (f,h))) = f ; ::_thesis: max (g,h) c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (max (g,h)) . x (max ((min (f,g)),(min (f,h)))) . x = max (((min (f,g)) . x),((min (f,h)) . x)) by Def4 .= max (((min (f,g)) . x),(min ((f . x),(h . x)))) by Def3 .= max ((min ((f . x),(g . x))),(min ((f . x),(h . x)))) by Def3 .= min ((f . x),(max ((g . x),(h . x)))) by XXREAL_0:38 ; then f . x <= max ((g . x),(h . x)) by A1, XXREAL_0:def_9; hence f . x <= (max (g,h)) . x by Def4; ::_thesis: verum end; theorem :: FUZZY_1:30 for C being non empty set for f, g, h being Membership_Func of C st g c= & min (g,h) = EMF C holds min (f,h) = EMF C proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= & min (g,h) = EMF C holds min (f,h) = EMF C let f, g, h be Membership_Func of C; ::_thesis: ( g c= & min (g,h) = EMF C implies min (f,h) = EMF C ) assume that A1: g c= and A2: min (g,h) = EMF C ; ::_thesis: min (f,h) = EMF C A3: for x being Element of C st x in C holds (min (f,h)) . x = (EMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,h)) . x = (EMF C) . x ) f . x <= g . x by A1, Def2; then min ((f . x),(h . x)) <= min ((g . x),(h . x)) by XXREAL_0:18; then min ((f . x),(h . x)) <= (min (g,h)) . x by Def3; then A4: (min (f,h)) . x <= (min (g,h)) . x by Def3; (EMF C) . x <= (min (f,h)) . x by Th16; hence ( x in C implies (min (f,h)) . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; ::_thesis: verum end; ( C = dom (min (f,h)) & C = dom (EMF C) ) by FUNCT_2:def_1; hence min (f,h) = EMF C by A3, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_1:31 for C being non empty set for f being Membership_Func of C st EMF C c= holds f = EMF C proof let C be non empty set ; ::_thesis: for f being Membership_Func of C st EMF C c= holds f = EMF C let f be Membership_Func of C; ::_thesis: ( EMF C c= implies f = EMF C ) f c= by Th14; hence ( EMF C c= implies f = EMF C ) by Lm1; ::_thesis: verum end; theorem :: FUZZY_1:32 for C being non empty set for f, g being Membership_Func of C holds ( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) ) let f, g be Membership_Func of C; ::_thesis: ( max (f,g) = EMF C iff ( f = EMF C & g = EMF C ) ) thus ( max (f,g) = EMF C implies ( f = EMF C & g = EMF C ) ) ::_thesis: ( f = EMF C & g = EMF C implies max (f,g) = EMF C ) proof assume A1: max (f,g) = EMF C ; ::_thesis: ( f = EMF C & g = EMF C ) A2: for x being Element of C st x in C holds f . x = (EMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies f . x = (EMF C) . x ) max ((f . x),(g . x)) = (EMF C) . x by A1, Def4; then A3: f . x <= (EMF C) . x by XXREAL_0:25; (EMF C) . x <= f . x by Th16; hence ( x in C implies f . x = (EMF C) . x ) by A3, XXREAL_0:1; ::_thesis: verum end; A4: for x being Element of C st x in C holds g . x = (EMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies g . x = (EMF C) . x ) max ((f . x),(g . x)) = (EMF C) . x by A1, Def4; then A5: g . x <= (EMF C) . x by XXREAL_0:25; (EMF C) . x <= g . x by Th16; hence ( x in C implies g . x = (EMF C) . x ) by A5, XXREAL_0:1; ::_thesis: verum end; ( C = dom f & C = dom (EMF C) ) by FUNCT_2:def_1; hence f = EMF C by A2, PARTFUN1:5; ::_thesis: g = EMF C ( C = dom g & C = dom (EMF C) ) by FUNCT_2:def_1; hence g = EMF C by A4, PARTFUN1:5; ::_thesis: verum end; assume ( f = EMF C & g = EMF C ) ; ::_thesis: max (f,g) = EMF C hence max (f,g) = EMF C ; ::_thesis: verum end; theorem :: FUZZY_1:33 for C being non empty set for f, g, h being Membership_Func of C holds ( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= ) ) ) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds ( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= ) ) ) let f, g, h be Membership_Func of C; ::_thesis: ( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= ) ) ) hereby ::_thesis: ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= ) implies f = max (g,h) ) assume A1: f = max (g,h) ; ::_thesis: ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= ) ) hence ( f c= & f c= ) by Th17; ::_thesis: for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= let h1 be Membership_Func of C; ::_thesis: ( h1 c= & h1 c= implies h1 c= ) assume A2: ( h1 c= & h1 c= ) ; ::_thesis: h1 c= thus h1 c= ::_thesis: verum proof let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= h1 . x ( g . x <= h1 . x & h . x <= h1 . x ) by A2, Def2; then max ((g . x),(h . x)) <= h1 . x by XXREAL_0:28; hence f . x <= h1 . x by A1, Def4; ::_thesis: verum end; end; assume that A3: ( f c= & f c= ) and A4: for h1 being Membership_Func of C st h1 c= & h1 c= holds h1 c= ; ::_thesis: f = max (g,h) ( max (g,h) c= & max (g,h) c= ) by Th17; then A5: max (g,h) c= by A4; f c= by A3, Th19; hence f = max (g,h) by A5, Lm1; ::_thesis: verum end; theorem :: FUZZY_1:34 for C being non empty set for f, g, h being Membership_Func of C holds ( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds f c= ) ) ) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds ( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds f c= ) ) ) let f, g, h be Membership_Func of C; ::_thesis: ( f = min (g,h) iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds f c= ) ) ) hereby ::_thesis: ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds f c= ) implies f = min (g,h) ) assume A1: f = min (g,h) ; ::_thesis: ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds f c= ) ) hence ( g c= & h c= ) by Th17; ::_thesis: for h1 being Membership_Func of C st g c= & h c= holds f c= let h1 be Membership_Func of C; ::_thesis: ( g c= & h c= implies f c= ) assume A2: ( g c= & h c= ) ; ::_thesis: f c= thus f c= ::_thesis: verum proof let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: h1 . x <= f . x ( h1 . x <= g . x & h1 . x <= h . x ) by A2, Def2; then min ((g . x),(h . x)) >= h1 . x by XXREAL_0:20; hence h1 . x <= f . x by A1, Def3; ::_thesis: verum end; end; assume that A3: ( g c= & h c= ) and A4: for h1 being Membership_Func of C st g c= & h c= holds f c= ; ::_thesis: f = min (g,h) ( g c= & h c= ) by Th17; then A5: f c= by A4; min (g,h) c= by A3, Th24; hence f = min (g,h) by A5, Lm1; ::_thesis: verum end; theorem :: FUZZY_1:35 for C being non empty set for f, g, h being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds g c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds g c= let f, g, h be Membership_Func of C; ::_thesis: ( max (g,h) c= & min (f,h) = EMF C implies g c= ) assume that A1: max (g,h) c= and A2: min (f,h) = EMF C ; ::_thesis: g c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . x <= g . x min (f,(max (g,h))) = f by A1, Th27; then f = max ((min (f,g)),(min (f,h))) by Th9 .= min (f,g) by A2, Th18 ; then f . x = min ((f . x),(g . x)) by Def3; hence f . x <= g . x by XXREAL_0:def_9; ::_thesis: verum end; Lm2: for C being non empty set for f, g being Membership_Func of C st g c= holds 1_minus f c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds 1_minus f c= let f, g be Membership_Func of C; ::_thesis: ( g c= implies 1_minus f c= ) assume A1: g c= ; ::_thesis: 1_minus f c= let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (1_minus g) . x <= (1_minus f) . x f . x <= g . x by A1, Def2; then 1 - (g . x) <= 1 - (f . x) by XREAL_1:10; then (1_minus g) . x <= 1 - (f . x) by Def5; hence (1_minus g) . x <= (1_minus f) . x by Def5; ::_thesis: verum end; theorem Th36: :: FUZZY_1:36 for C being non empty set for f, g being Membership_Func of C holds ( g c= iff 1_minus f c= ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( g c= iff 1_minus f c= ) let f, g be Membership_Func of C; ::_thesis: ( g c= iff 1_minus f c= ) ( 1_minus (1_minus f) = f & 1_minus (1_minus g) = g ) ; hence ( g c= iff 1_minus f c= ) by Lm2; ::_thesis: verum end; theorem :: FUZZY_1:37 for C being non empty set for f, g being Membership_Func of C st 1_minus g c= holds 1_minus f c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st 1_minus g c= holds 1_minus f c= let f, g be Membership_Func of C; ::_thesis: ( 1_minus g c= implies 1_minus f c= ) 1_minus (1_minus f) = f ; hence ( 1_minus g c= implies 1_minus f c= ) by Th36; ::_thesis: verum end; theorem :: FUZZY_1:38 for C being non empty set for f, g being Membership_Func of C holds 1_minus f c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus f c= let f, g be Membership_Func of C; ::_thesis: 1_minus f c= max (f,g) c= by Th17; hence 1_minus f c= by Th36; ::_thesis: verum end; theorem :: FUZZY_1:39 for C being non empty set for f, g being Membership_Func of C holds 1_minus (min (f,g)) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus (min (f,g)) c= let f, g be Membership_Func of C; ::_thesis: 1_minus (min (f,g)) c= f c= by Th17; hence 1_minus (min (f,g)) c= by Th36; ::_thesis: verum end; theorem Th40: :: FUZZY_1:40 for C being non empty set holds ( 1_minus (EMF C) = UMF C & 1_minus (UMF C) = EMF C ) proof let C be non empty set ; ::_thesis: ( 1_minus (EMF C) = UMF C & 1_minus (UMF C) = EMF C ) A1: for x being Element of C st x in C holds (1_minus (EMF C)) . x = (UMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies (1_minus (EMF C)) . x = (UMF C) . x ) (1_minus (EMF C)) . x = 1 - ((EMF C) . x) by Def5 .= 1 - 0 by FUNCT_3:def_3 .= 1 ; hence ( x in C implies (1_minus (EMF C)) . x = (UMF C) . x ) by FUNCT_3:def_3; ::_thesis: verum end; ( C = dom (1_minus (EMF C)) & C = dom (UMF C) ) by FUNCT_2:def_1; hence 1_minus (EMF C) = UMF C by A1, PARTFUN1:5; ::_thesis: 1_minus (UMF C) = EMF C A2: for x being Element of C st x in C holds (1_minus (UMF C)) . x = (EMF C) . x proof let x be Element of C; ::_thesis: ( x in C implies (1_minus (UMF C)) . x = (EMF C) . x ) (1_minus (UMF C)) . x = 1 - ((UMF C) . x) by Def5 .= 1 - 1 by FUNCT_3:def_3 .= 0 ; hence ( x in C implies (1_minus (UMF C)) . x = (EMF C) . x ) by FUNCT_3:def_3; ::_thesis: verum end; ( C = dom (1_minus (UMF C)) & C = dom (EMF C) ) by FUNCT_2:def_1; hence 1_minus (UMF C) = EMF C by A2, PARTFUN1:5; ::_thesis: verum end; definition let C be non empty set ; let h, g be Membership_Func of C; funch \+\ g -> Membership_Func of C equals :: FUZZY_1:def 8 max ((min (h,(1_minus g))),(min ((1_minus h),g))); coherence max ((min (h,(1_minus g))),(min ((1_minus h),g))) is Membership_Func of C ; commutativity for b1, h, g being Membership_Func of C st b1 = max ((min (h,(1_minus g))),(min ((1_minus h),g))) holds b1 = max ((min (g,(1_minus h))),(min ((1_minus g),h))) ; end; :: deftheorem defines \+\ FUZZY_1:def_8_:_ for C being non empty set for h, g being Membership_Func of C holds h \+\ g = max ((min (h,(1_minus g))),(min ((1_minus h),g))); theorem :: FUZZY_1:41 for C being non empty set for f being Membership_Func of C holds f \+\ (EMF C) = f proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds f \+\ (EMF C) = f let f be Membership_Func of C; ::_thesis: f \+\ (EMF C) = f thus f \+\ (EMF C) = max ((min (f,(UMF C))),(min ((1_minus f),(EMF C)))) by Th40 .= max (f,(min ((1_minus f),(EMF C)))) by Th18 .= max (f,(EMF C)) by Th18 .= f by Th18 ; ::_thesis: verum end; theorem :: FUZZY_1:42 for C being non empty set for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f let f be Membership_Func of C; ::_thesis: f \+\ (UMF C) = 1_minus f thus f \+\ (UMF C) = max ((min (f,(EMF C))),(min ((1_minus f),(UMF C)))) by Th40 .= max ((EMF C),(min ((1_minus f),(UMF C)))) by Th18 .= min ((1_minus f),(UMF C)) by Th18 .= 1_minus f by Th18 ; ::_thesis: verum end; theorem :: FUZZY_1:43 for C being non empty set for f, g, h being Membership_Func of C holds min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f))) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f))) let f, g, h be Membership_Func of C; ::_thesis: min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((max ((min (f,g)),(min (g,h)))),(min (h,f))) thus min ((min ((max (f,g)),(max (g,h)))),(max (h,f))) = max ((min ((min ((max (f,g)),(max (g,h)))),h)),(min ((min ((max (f,g)),(max (g,h)))),f))) by Th9 .= max ((min ((max (f,g)),(min ((max (g,h)),h)))),(min ((min ((max (f,g)),(max (g,h)))),f))) by Th7 .= max ((min ((max (f,g)),(min ((max (h,g)),h)))),(min ((min ((max (f,g)),f)),(max (g,h))))) by Th7 .= max ((min ((max (f,g)),h)),(min ((min ((max (f,g)),f)),(max (g,h))))) by Th8 .= max ((min ((max (f,g)),h)),(min (f,(max (g,h))))) by Th8 .= max ((min (h,(max (f,g)))),(max ((min (f,g)),(min (f,h))))) by Th9 .= max ((max ((min (f,g)),(min (f,h)))),(max ((min (h,f)),(min (h,g))))) by Th9 .= max ((max ((max ((min (f,g)),(min (f,h)))),(min (f,h)))),(min (h,g))) by Th7 .= max ((max ((min (f,g)),(max ((min (f,h)),(min (f,h)))))),(min (h,g))) by Th7 .= max ((max ((min (f,g)),(min (g,h)))),(min (h,f))) by Th7 ; ::_thesis: verum end; theorem :: FUZZY_1:44 for C being non empty set for f, g being Membership_Func of C holds 1_minus (f \+\ g) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus (f \+\ g) c= let f, g be Membership_Func of C; ::_thesis: 1_minus (f \+\ g) c= set f1 = 1_minus f; set g1 = 1_minus g; let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x <= (1_minus (f \+\ g)) . x 1_minus (f \+\ g) = min ((1_minus (min (f,(1_minus g)))),(1_minus (min ((1_minus f),g)))) by Th11 .= min ((max ((1_minus f),(1_minus (1_minus g)))),(1_minus (min ((1_minus f),g)))) by Th11 .= min ((max ((1_minus f),g)),(max ((1_minus (1_minus f)),(1_minus g)))) by Th11 .= max ((min ((max ((1_minus f),g)),f)),(min ((max ((1_minus f),g)),(1_minus g)))) by Th9 .= max ((max ((min (f,(1_minus f))),(min (f,g)))),(min ((max ((1_minus f),g)),(1_minus g)))) by Th9 .= max ((max ((min (f,(1_minus f))),(min (f,g)))),(max ((min ((1_minus g),(1_minus f))),(min ((1_minus g),g))))) by Th9 .= max ((max ((max ((min (f,g)),(min (f,(1_minus f))))),(min ((1_minus g),(1_minus f))))),(min ((1_minus g),g))) by Th7 .= max ((max ((max ((min ((1_minus g),(1_minus f))),(min (f,g)))),(min (f,(1_minus f))))),(min ((1_minus g),g))) by Th7 .= max ((max ((min ((1_minus g),(1_minus f))),(min (f,g)))),(max ((min (f,(1_minus f))),(min ((1_minus g),g))))) by Th7 ; then (1_minus (f \+\ g)) . x = max (((max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x),((max ((min (f,(1_minus f))),(min ((1_minus g),g)))) . x)) by Def4; hence (max ((min (f,g)),(min ((1_minus f),(1_minus g))))) . x <= (1_minus (f \+\ g)) . x by XXREAL_0:25; ::_thesis: verum end; theorem :: FUZZY_1:45 for C being non empty set for f, g being Membership_Func of C holds max (f,g) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds max (f,g) c= let f, g be Membership_Func of C; ::_thesis: max (f,g) c= set f1 = 1_minus f; set g1 = 1_minus g; let x be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max ((f \+\ g),(min (f,g)))) . x <= (max (f,g)) . x max ((f \+\ g),(min (f,g))) = max ((min (f,(1_minus g))),(max ((min ((1_minus f),g)),(min (f,g))))) by Th7 .= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),(max (g,(min ((1_minus f),g))))))) by Th9 .= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),g))) by Th8 .= min ((max ((min (f,(1_minus g))),(max (f,(min ((1_minus f),g)))))),(max ((min (f,(1_minus g))),g))) by Th9 .= min ((max ((max (f,(min (f,(1_minus g))))),(min ((1_minus f),g)))),(max ((min (f,(1_minus g))),g))) by Th7 .= min ((max (f,(min ((1_minus f),g)))),(max ((min (f,(1_minus g))),g))) by Th8 .= min ((min ((max (f,(1_minus f))),(max (f,g)))),(max (g,(min (f,(1_minus g)))))) by Th9 .= min ((min ((max (f,(1_minus f))),(max (f,g)))),(min ((max (g,f)),(max (g,(1_minus g)))))) by Th9 .= min ((min ((min ((max (f,(1_minus f))),(max (f,g)))),(max (g,f)))),(max (g,(1_minus g)))) by Th7 .= min ((min ((max (f,(1_minus f))),(min ((max (f,g)),(max (f,g)))))),(max (g,(1_minus g)))) by Th7 .= min ((max (f,g)),(min ((max (f,(1_minus f))),(max (g,(1_minus g)))))) by Th7 ; then (max ((f \+\ g),(min (f,g)))) . x = min (((max (f,g)) . x),((min ((max (f,(1_minus f))),(max (g,(1_minus g))))) . x)) by Def3; hence (max ((f \+\ g),(min (f,g)))) . x <= (max (f,g)) . x by XXREAL_0:17; ::_thesis: verum end; theorem :: FUZZY_1:46 for C being non empty set for f being Membership_Func of C holds f \+\ f = min (f,(1_minus f)) ; definition let C be non empty set ; let h, g be Membership_Func of C; func ab_difMF (h,g) -> Membership_Func of C means :: FUZZY_1:def 9 for c being Element of C holds it . c = abs ((h . c) - (g . c)); existence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) proof defpred S1[ set , set ] means \$2 = abs ((h . \$1) - (g . \$1)); A1: for x, y1, y2 being set st x in C & S1[x,y1] & S1[x,y2] holds y1 = y2 ; A2: for x, y being set st x in C & S1[x,y] holds y in REAL ; consider IT being PartFunc of C,REAL such that A3: ( ( for x being set holds ( x in dom IT iff ( x in C & ex y being set st S1[x,y] ) ) ) & ( for x being set st x in dom IT holds S1[x,IT . x] ) ) from PARTFUN1:sch_2(A2, A1); for x being set st x in C holds x in dom IT proof let x be set ; ::_thesis: ( x in C implies x in dom IT ) A4: ex y being set st y = abs ((h . x) - (g . x)) ; assume x in C ; ::_thesis: x in dom IT hence x in dom IT by A3, A4; ::_thesis: verum end; then C c= dom IT by TARSKI:def_3; then A5: dom IT = C by XBOOLE_0:def_10; then A6: for c being Element of C holds IT . c = abs ((h . c) - (g . c)) by A3; A7: rng g c= [.0,1.] by RELAT_1:def_19; A8: rng h c= [.0,1.] by RELAT_1:def_19; for y being set st y in rng IT holds y in [.0,1.] proof reconsider A = [.0,1.] as non empty closed_interval Subset of REAL by MEASURE5:14; let y be set ; ::_thesis: ( y in rng IT implies y in [.0,1.] ) assume y in rng IT ; ::_thesis: y in [.0,1.] then consider x being Element of C such that A9: x in dom IT and A10: y = IT . x by PARTFUN1:3; 0 <= abs ((h . x) - (g . x)) by COMPLEX1:46; then A11: 0 <= IT . x by A3, A9; A12: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A13: 0 = lower_bound A by INTEGRA1:5; A14: x in C ; then x in dom h by FUNCT_2:def_1; then A15: h . x in rng h by FUNCT_1:def_3; x in dom g by A14, FUNCT_2:def_1; then A16: g . x in rng g by FUNCT_1:def_3; then 0 <= g . x by A7, A13, INTEGRA2:1; then A17: 1 - 0 >= 1 - (g . x) by XREAL_1:10; A18: 1 = upper_bound A by A12, INTEGRA1:5; then g . x <= 1 by A7, A16, INTEGRA2:1; then A19: - (g . x) >= - 1 by XREAL_1:24; 0 <= h . x by A8, A13, A15, INTEGRA2:1; then 0 - (g . x) <= (h . x) - (g . x) by XREAL_1:9; then A20: - 1 <= (h . x) - (g . x) by A19, XXREAL_0:2; h . x <= 1 by A8, A18, A15, INTEGRA2:1; then (h . x) - (g . x) <= 1 - (g . x) by XREAL_1:9; then (h . x) - (g . x) <= 1 by A17, XXREAL_0:2; then abs ((h . x) - (g . x)) <= 1 by A20, ABSVALUE:5; then IT . x <= 1 by A3, A9; hence y in [.0,1.] by A10, A13, A18, A11, INTEGRA2:1; ::_thesis: verum end; then A21: rng IT c= [.0,1.] by TARSKI:def_3; IT is total by A5, PARTFUN1:def_2; then IT is Membership_Func of C by A21, RELAT_1:def_19; hence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) by A6; ::_thesis: verum end; uniqueness for b1, b2 being Membership_Func of C st ( for c being Element of C holds b1 . c = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds b2 . c = abs ((h . c) - (g . c)) ) holds b1 = b2 proof let F, G be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds F . c = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds G . c = abs ((h . c) - (g . c)) ) implies F = G ) assume that A22: for c being Element of C holds F . c = abs ((h . c) - (g . c)) and A23: for c being Element of C holds G . c = abs ((h . c) - (g . c)) ; ::_thesis: F = G A24: for c being Element of C st c in C holds F . c = G . c proof let c be Element of C; ::_thesis: ( c in C implies F . c = G . c ) F . c = abs ((h . c) - (g . c)) by A22; hence ( c in C implies F . c = G . c ) by A23; ::_thesis: verum end; ( C = dom F & C = dom G ) by FUNCT_2:def_1; hence F = G by A24, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem defines ab_difMF FUZZY_1:def_9_:_ for C being non empty set for h, g, b4 being Membership_Func of C holds ( b4 = ab_difMF (h,g) iff for c being Element of C holds b4 . c = abs ((h . c) - (g . c)) );