:: FUZZY_2 semantic presentation begin theorem Th1: :: FUZZY_2:1 for C being non empty set for x being Element of C for h being Membership_Func of C holds ( 0 <= h . x & h . x <= 1 ) proof let C be non empty set ; ::_thesis: for x being Element of C for h being Membership_Func of C holds ( 0 <= h . x & h . x <= 1 ) let x be Element of C; ::_thesis: for h being Membership_Func of C holds ( 0 <= h . x & h . x <= 1 ) let h be Membership_Func of C; ::_thesis: ( 0 <= h . x & h . x <= 1 ) (EMF C) . x = 0 by FUNCT_3:def_3; hence 0 <= h . x by FUZZY_1:16; ::_thesis: h . x <= 1 (UMF C) . x = 1 by FUNCT_3:def_3; hence h . x <= 1 by FUZZY_1:16; ::_thesis: verum end; theorem :: FUZZY_2:2 for C being non empty set for f, h, g being Membership_Func of C st h c= holds max (f,(min (g,h))) = min ((max (f,g)),h) proof let C be non empty set ; ::_thesis: for f, h, g being Membership_Func of C st h c= holds max (f,(min (g,h))) = min ((max (f,g)),h) let f, h, g be Membership_Func of C; ::_thesis: ( h c= implies max (f,(min (g,h))) = min ((max (f,g)),h) ) assume A1: h c= ; ::_thesis: max (f,(min (g,h))) = min ((max (f,g)),h) thus max (f,(min (g,h))) = min ((max (f,g)),(max (f,h))) by FUZZY_1:9 .= min ((max (f,g)),h) by A1, FUZZY_1:22 ; ::_thesis: verum end; definition let C be non empty set ; let f, g be Membership_Func of C; funcf \ g -> Membership_Func of C equals :: FUZZY_2:def 1 min (f,(1_minus g)); correctness coherence min (f,(1_minus g)) is Membership_Func of C; ; end; :: deftheorem defines \ FUZZY_2:def_1_:_ for C being non empty set for f, g being Membership_Func of C holds f \ g = min (f,(1_minus g)); theorem :: FUZZY_2:3 for C being non empty set for f, g being Membership_Func of C holds 1_minus (f \ g) = max ((1_minus f),g) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds 1_minus (f \ g) = max ((1_minus f),g) let f, g be Membership_Func of C; ::_thesis: 1_minus (f \ g) = max ((1_minus f),g) thus 1_minus (f \ g) = max ((1_minus f),(1_minus (1_minus g))) by FUZZY_1:11 .= max ((1_minus f),g) ; ::_thesis: verum end; theorem Th4: :: FUZZY_2:4 for C being non empty set for f, g, h being Membership_Func of C st g c= holds g \ h c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= holds g \ h c= let f, g, h be Membership_Func of C; ::_thesis: ( g c= implies g \ h c= ) assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def_2 ::_thesis: g \ h c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f \ h) . c <= (g \ h) . c f . c <= g . c by A1; then min ((f . c),((1_minus h) . c)) <= min ((g . c),((1_minus h) . c)) by XXREAL_0:18; then (f \ h) . c <= min ((g . c),((1_minus h) . c)) by FUZZY_1:5; hence (f \ h) . c <= (g \ h) . c by FUZZY_1:5; ::_thesis: verum end; theorem :: FUZZY_2:5 for C being non empty set for f, g, h being Membership_Func of C st g c= holds h \ f c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st g c= holds h \ f c= let f, g, h be Membership_Func of C; ::_thesis: ( g c= implies h \ f c= ) assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def_2 ::_thesis: h \ f c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (h \ g) . c <= (h \ f) . c f . c <= g . c by A1; then 1 - (f . c) >= 1 - (g . c) by XREAL_1:10; then (1_minus g) . c <= 1 - (f . c) by FUZZY_1:def_5; then (1_minus g) . c <= (1_minus f) . c by FUZZY_1:def_5; then min (((1_minus g) . c),(h . c)) <= min (((1_minus f) . c),(h . c)) by XXREAL_0:18; then (h \ g) . c <= min (((1_minus f) . c),(h . c)) by FUZZY_1:5; hence (h \ g) . c <= (h \ f) . c by FUZZY_1:5; ::_thesis: verum end; theorem :: FUZZY_2:6 for C being non empty set for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds g \ h 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 g \ h c= let f, g, h, h1 be Membership_Func of C; ::_thesis: ( g c= & h1 c= implies g \ h c= ) assume that A1: for c being Element of C holds f . c <= g . c and A2: for c being Element of C holds h . c <= h1 . c ; :: according to FUZZY_1:def_2 ::_thesis: g \ h c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f \ h1) . c <= (g \ h) . c h . c <= h1 . c by A2; then A3: 1 - (h . c) >= 1 - (h1 . c) by XREAL_1:10; f . c <= g . c by A1; then min ((f . c),(1 - (h1 . c))) <= min ((g . c),(1 - (h . c))) by A3, XXREAL_0:18; then min ((f . c),((1_minus h1) . c)) <= min ((g . c),(1 - (h . c))) by FUZZY_1:def_5; then min ((f . c),((1_minus h1) . c)) <= min ((g . c),((1_minus h) . c)) by FUZZY_1:def_5; then (min (f,(1_minus h1))) . c <= min ((g . c),((1_minus h) . c)) by FUZZY_1:5; hence (f \ h1) . c <= (g \ h) . c by FUZZY_1:5; ::_thesis: verum end; theorem :: FUZZY_2:7 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) = min (f,(UMF C)) by FUZZY_1:40 .= f by FUZZY_1:18 ; ::_thesis: verum end; theorem :: FUZZY_2:8 for C being non empty set for f, g being Membership_Func of C holds f \ (min (f,g)) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds f \ (min (f,g)) c= let f, g be Membership_Func of C; ::_thesis: f \ (min (f,g)) c= f \ (min (f,g)) = min (f,(max ((1_minus f),(1_minus g)))) by FUZZY_1:11 .= max ((min (f,(1_minus f))),(f \ g)) by FUZZY_1:9 ; hence f \ (min (f,g)) c= by FUZZY_1:17; ::_thesis: verum end; theorem :: FUZZY_2:9 for C being non empty set for f, g being Membership_Func of C holds f c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds f c= let f, g be Membership_Func of C; ::_thesis: f c= A1: f c= by FUZZY_1:17; f c= by FUZZY_1:17; hence f c= by A1, FUZZY_1:19; ::_thesis: verum end; theorem :: FUZZY_2:10 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= max (f,(g \ f)) = min ((max (f,g)),(max (f,(1_minus f)))) by FUZZY_1:9; hence max (f,g) c= by FUZZY_1:17; ::_thesis: verum end; theorem :: FUZZY_2:11 for C being non empty set for f, g, h being Membership_Func of C holds f \ (g \ h) = max ((f \ g),(min (f,h))) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f \ (g \ h) = max ((f \ g),(min (f,h))) let f, g, h be Membership_Func of C; ::_thesis: f \ (g \ h) = max ((f \ g),(min (f,h))) f \ (g \ h) = min (f,(max ((1_minus g),(1_minus (1_minus h))))) by FUZZY_1:11 .= max ((min (f,(1_minus g))),(min (f,h))) by FUZZY_1:9 ; hence f \ (g \ h) = max ((f \ g),(min (f,h))) ; ::_thesis: verum end; theorem :: FUZZY_2:12 for C being non empty set for f, g being Membership_Func of C holds f \ (f \ g) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds f \ (f \ g) c= let f, g be Membership_Func of C; ::_thesis: f \ (f \ g) c= f \ (f \ g) = min (f,(max ((1_minus f),(1_minus (1_minus g))))) by FUZZY_1:11 .= max ((min (f,(1_minus f))),(min (f,g))) by FUZZY_1:9 ; hence f \ (f \ g) c= by FUZZY_1:17; ::_thesis: verum end; theorem :: FUZZY_2:13 for C being non empty set for f, g being Membership_Func of C holds (max (f,g)) \ g c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds (max (f,g)) \ g c= let f, g be Membership_Func of C; ::_thesis: (max (f,g)) \ g c= max (f,g) c= by FUZZY_1:17; hence (max (f,g)) \ g c= by Th4; ::_thesis: verum end; theorem :: FUZZY_2:14 for C being non empty set for f, g, h being Membership_Func of C holds f \ (max (g,h)) = min ((f \ g),(f \ h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f \ (max (g,h)) = min ((f \ g),(f \ h)) let f, g, h be Membership_Func of C; ::_thesis: f \ (max (g,h)) = min ((f \ g),(f \ h)) thus f \ (max (g,h)) = min ((min (f,f)),(min ((1_minus g),(1_minus h)))) by FUZZY_1:11 .= min (f,(min (f,(min ((1_minus g),(1_minus h)))))) by FUZZY_1:7 .= min (f,(min ((min (f,(1_minus g))),(1_minus h)))) by FUZZY_1:7 .= min ((f \ g),(f \ h)) by FUZZY_1:7 ; ::_thesis: verum end; theorem :: FUZZY_2:15 for C being non empty set for f, g, h being Membership_Func of C holds f \ (min (g,h)) = max ((f \ g),(f \ h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f \ (min (g,h)) = max ((f \ g),(f \ h)) let f, g, h be Membership_Func of C; ::_thesis: f \ (min (g,h)) = max ((f \ g),(f \ h)) thus f \ (min (g,h)) = min (f,(max ((1_minus g),(1_minus h)))) by FUZZY_1:11 .= max ((f \ g),(f \ h)) by FUZZY_1:9 ; ::_thesis: verum end; theorem :: FUZZY_2:16 for C being non empty set for f, g, h being Membership_Func of C holds (f \ g) \ h = f \ (max (g,h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (f \ g) \ h = f \ (max (g,h)) let f, g, h be Membership_Func of C; ::_thesis: (f \ g) \ h = f \ (max (g,h)) thus (f \ g) \ h = min (f,(min ((1_minus g),(1_minus h)))) by FUZZY_1:7 .= f \ (max (g,h)) by FUZZY_1:11 ; ::_thesis: verum end; theorem :: FUZZY_2:17 for C being non empty set for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c= let f, g be Membership_Func of C; ::_thesis: (max (f,g)) \ (min (f,g)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c ((max (f,g)) \ (min (f,g))) . c = (min ((max (f,g)),(max ((1_minus f),(1_minus g))))) . c by FUZZY_1:11 .= (max ((min ((max (f,g)),(1_minus f))),(min ((max (f,g)),(1_minus g))))) . c by FUZZY_1:9 .= (max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(min ((1_minus g),(max (f,g)))))) . c by FUZZY_1:9 .= (max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(max ((min ((1_minus g),f)),(min ((1_minus g),g)))))) . c by FUZZY_1:9 .= (max ((max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(min ((1_minus g),f)))),(min ((1_minus g),g)))) . c by FUZZY_1:7 .= (max ((max ((min ((1_minus f),f)),(max ((min ((1_minus f),g)),(min ((1_minus g),f)))))),(min ((1_minus g),g)))) . c by FUZZY_1:7 .= (max ((max ((min ((1_minus f),g)),(min ((1_minus g),f)))),(max ((min ((1_minus f),f)),(min ((1_minus g),g)))))) . c by FUZZY_1:7 .= max (((f \+\ g) . c),((max ((min ((1_minus f),f)),(min ((1_minus g),g)))) . c)) by FUZZY_1:5 ; hence (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c by XXREAL_0:25; ::_thesis: verum end; theorem :: FUZZY_2:18 for C being non empty set for f, g, h being Membership_Func of C st h c= & h c= holds h c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C st h c= & h c= holds h c= let f, g, h be Membership_Func of C; ::_thesis: ( h c= & h c= implies h c= ) assume that A1: for c being Element of C holds (f \ g) . c <= h . c and A2: for c being Element of C holds (g \ f) . c <= h . c ; :: according to FUZZY_1:def_2 ::_thesis: h c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f \+\ g) . c <= h . c A3: (min (g,(1_minus f))) . c <= h . c by A2; (min (f,(1_minus g))) . c <= h . c by A1; then max (((min (f,(1_minus g))) . c),((min (g,(1_minus f))) . c)) <= max ((h . c),(h . c)) by A3, XXREAL_0:26; hence (f \+\ g) . c <= h . c by FUZZY_1:5; ::_thesis: verum end; theorem :: FUZZY_2:19 for C being non empty set for f, g, h being Membership_Func of C holds (min (f,g)) \ (min (f,h)) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (min (f,g)) \ (min (f,h)) c= let f, g, h be Membership_Func of C; ::_thesis: (min (f,g)) \ (min (f,h)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,(g \ h))) . c <= ((min (f,g)) \ (min (f,h))) . c (1_minus h) . c <= max (((1_minus f) . c),((1_minus h) . c)) by XXREAL_0:25; then min (((min (f,g)) . c),((1_minus h) . c)) <= min (((min (f,g)) . c),(max (((1_minus f) . c),((1_minus h) . c)))) by XXREAL_0:18; then min (((min (f,g)) . c),((1_minus h) . c)) <= min (((min (f,g)) . c),((max ((1_minus f),(1_minus h))) . c)) by FUZZY_1:5; then A1: min (((min (f,g)) . c),((1_minus h) . c)) <= (min ((min (f,g)),(max ((1_minus f),(1_minus h))))) . c by FUZZY_1:5; (min (f,(g \ h))) . c = (min ((min (f,g)),(1_minus h))) . c by FUZZY_1:7 .= min (((min (f,g)) . c),((1_minus h) . c)) by FUZZY_1:5 ; hence (min (f,(g \ h))) . c <= ((min (f,g)) \ (min (f,h))) . c by A1, FUZZY_1:11; ::_thesis: verum end; theorem Th20: :: FUZZY_2:20 for C being non empty set for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds (max (f,g)) \ (min (f,g)) c= let f, g be Membership_Func of C; ::_thesis: (max (f,g)) \ (min (f,g)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c ((max (f,g)) \ (min (f,g))) . c = (min ((max (f,g)),(max ((1_minus f),(1_minus g))))) . c by FUZZY_1:11 .= (max ((min ((max (f,g)),(1_minus f))),(min ((max (f,g)),(1_minus g))))) . c by FUZZY_1:9 .= (max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(min ((1_minus g),(max (f,g)))))) . c by FUZZY_1:9 .= (max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(max ((min ((1_minus g),f)),(min ((1_minus g),g)))))) . c by FUZZY_1:9 .= (max ((max ((max ((min ((1_minus f),f)),(min ((1_minus f),g)))),(min ((1_minus g),g)))),(min ((1_minus g),f)))) . c by FUZZY_1:7 .= (max ((max ((max ((min ((1_minus f),f)),(min ((1_minus g),g)))),(min ((1_minus f),g)))),(min ((1_minus g),f)))) . c by FUZZY_1:7 .= (max ((max ((min ((1_minus f),f)),(min ((1_minus g),g)))),(max ((min ((1_minus f),g)),(min ((1_minus g),f)))))) . c by FUZZY_1:7 .= max (((max ((min ((1_minus f),f)),(min ((1_minus g),g)))) . c),((f \+\ g) . c)) by FUZZY_1:5 ; hence (f \+\ g) . c <= ((max (f,g)) \ (min (f,g))) . c by XXREAL_0:25; ::_thesis: verum end; theorem Th21: :: FUZZY_2:21 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= (max (f,g)) \ (min (f,g)) c= by Th20; then 1_minus (f \+\ g) c= by FUZZY_1:36; then 1_minus (f \+\ g) c= by FUZZY_1:11; hence 1_minus (f \+\ g) c= ; ::_thesis: verum end; theorem :: FUZZY_2:22 for C being non empty set for f, g, h being Membership_Func of C holds (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h)))) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h)))) let f, g, h be Membership_Func of C; ::_thesis: (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h)))) set f1 = 1_minus f; set g1 = 1_minus g; set h1 = 1_minus h; (max ((min (f,(1_minus g))),(min ((1_minus f),g)))) \ h = max ((min ((1_minus h),(min (f,(1_minus g))))),(min ((1_minus h),(min ((1_minus f),g))))) by FUZZY_1:9 .= max ((min ((min ((1_minus h),(1_minus g))),f)),(min ((1_minus h),(min ((1_minus f),g))))) by FUZZY_1:7 .= max ((min ((min ((1_minus h),(1_minus g))),f)),(min ((min ((1_minus h),(1_minus f))),g))) by FUZZY_1:7 .= max ((min (f,(1_minus (max (h,g))))),(min (g,(min ((1_minus h),(1_minus f)))))) by FUZZY_1:11 .= max ((f \ (max (h,g))),(g \ (max (f,h)))) by FUZZY_1:11 ; hence (f \+\ g) \ h = max ((f \ (max (g,h))),(g \ (max (f,h)))) ; ::_thesis: verum end; theorem :: FUZZY_2:23 for C being non empty set for f, g, h being Membership_Func of C holds f \ (g \+\ h) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f \ (g \+\ h) c= let f, g, h be Membership_Func of C; ::_thesis: f \ (g \+\ h) c= max ((f \ (max (g,h))),(min ((min (f,g)),h))) = max ((min (f,(1_minus (max (g,h))))),(min (f,(min (g,h))))) by FUZZY_1:7 .= min (f,(max ((1_minus (max (g,h))),(min (g,h))))) by FUZZY_1:9 ; hence f \ (g \+\ h) c= by Th21, FUZZY_1:25; ::_thesis: verum end; theorem :: FUZZY_2:24 for C being non empty set for f, g being Membership_Func of C st g c= holds g c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st g c= holds g c= let f, g be Membership_Func of C; ::_thesis: ( g c= implies g c= ) assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def_2 ::_thesis: g c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,(g \ f))) . c <= g . c A2: f . c <= g . c by A1; (max (f,(g \ f))) . c = (min ((max (f,g)),(max (f,(1_minus f))))) . c by FUZZY_1:9 .= min (((max (f,g)) . c),((max (f,(1_minus f))) . c)) by FUZZY_1:5 .= min ((max ((f . c),(g . c))),((max (f,(1_minus f))) . c)) by FUZZY_1:5 .= min ((g . c),((max (f,(1_minus f))) . c)) by A2, XXREAL_0:def_10 ; hence (max (f,(g \ f))) . c <= g . c by XXREAL_0:17; ::_thesis: verum end; theorem :: FUZZY_2:25 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 c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max ((f \+\ g),(min (f,g)))) . c <= (max (f,g)) . c max ((f \+\ g),(min (f,g))) = max ((min (f,(1_minus g))),(max ((min ((1_minus f),g)),(min (f,g))))) by FUZZY_1:7 .= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),(max ((min ((1_minus f),g)),g))))) by FUZZY_1:9 .= max ((min (f,(1_minus g))),(min ((max ((min ((1_minus f),g)),f)),g))) by FUZZY_1:8 .= min ((max ((min (f,(1_minus g))),(max ((min ((1_minus f),g)),f)))),(max ((min (f,(1_minus g))),g))) by FUZZY_1:9 ; then (max ((f \+\ g),(min (f,g)))) . c = min (((max ((min (f,(1_minus g))),(max ((min ((1_minus f),g)),f)))) . c),((max ((min (f,(1_minus g))),g)) . c)) by FUZZY_1:5; then A1: (max ((f \+\ g),(min (f,g)))) . c <= (max ((min (f,(1_minus g))),g)) . c by XXREAL_0:17; (max ((min (f,(1_minus g))),g)) . c = (min ((max (g,f)),(max (g,(1_minus g))))) . c by FUZZY_1:9 .= min (((max (f,g)) . c),((max (g,(1_minus g))) . c)) by FUZZY_1:5 ; then (max ((min (f,(1_minus g))),g)) . c <= (max (f,g)) . c by XXREAL_0:17; hence (max ((f \+\ g),(min (f,g)))) . c <= (max (f,g)) . c by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th26: :: FUZZY_2:26 for C being non empty set for f, g being Membership_Func of C st f \ g = EMF C holds g c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st f \ g = EMF C holds g c= let f, g be Membership_Func of C; ::_thesis: ( f \ g = EMF C implies g c= ) assume A1: f \ g = EMF C ; ::_thesis: g c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . c <= g . c A2: min ((f . c),((1_minus g) . c)) = (EMF C) . c by A1, FUZZY_1:5; percases ( f . c = (EMF C) . c or (1_minus g) . c = (EMF C) . c ) by A2, XXREAL_0:15; suppose f . c = (EMF C) . c ; ::_thesis: f . c <= g . c hence f . c <= g . c by FUZZY_1:16; ::_thesis: verum end; supposeA3: (1_minus g) . c = (EMF C) . c ; ::_thesis: f . c <= g . c g . c = (1_minus (1_minus g)) . c .= 1 - ((1_minus g) . c) by FUZZY_1:def_5 .= (1_minus (EMF C)) . c by A3, FUZZY_1:def_5 .= (UMF C) . c by FUZZY_1:40 ; hence f . c <= g . c by FUZZY_1:16; ::_thesis: verum end; end; end; theorem Th27: :: FUZZY_2:27 for C being non empty set for f, g being Membership_Func of C st min (f,g) = EMF C holds f \ g = f proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C st min (f,g) = EMF C holds f \ g = f let f, g be Membership_Func of C; ::_thesis: ( min (f,g) = EMF C implies f \ g = f ) A1: C = dom f by FUNCT_2:def_1; assume A2: min (f,g) = EMF C ; ::_thesis: f \ g = f A3: for x being Element of C st x in C holds (min (f,(1_minus g))) . x = f . x proof let x be Element of C; ::_thesis: ( x in C implies (min (f,(1_minus g))) . x = f . x ) A4: (EMF C) . x = min ((f . x),(g . x)) by A2, FUZZY_1:5; percases ( f . x = (EMF C) . x or g . x = (EMF C) . x ) by A4, XXREAL_0:15; supposeA5: f . x = (EMF C) . x ; ::_thesis: ( x in C implies (min (f,(1_minus g))) . x = f . x ) (min (f,(1_minus g))) . x = min ((f . x),((1_minus g) . x)) by FUZZY_1:5 .= (min ((1_minus g),(EMF C))) . x by A5, FUZZY_1:5 .= (EMF C) . x by FUZZY_1:18 ; hence ( x in C implies (min (f,(1_minus g))) . x = f . x ) by A5; ::_thesis: verum end; supposeA6: g . x = (EMF C) . x ; ::_thesis: ( x in C implies (min (f,(1_minus g))) . x = f . x ) (min (f,(1_minus g))) . x = min ((f . x),((1_minus g) . x)) by FUZZY_1:5 .= min ((f . x),(1 - ((EMF C) . x))) by A6, FUZZY_1:def_5 .= min ((f . x),((1_minus (EMF C)) . x)) by FUZZY_1:def_5 .= min ((f . x),((UMF C) . x)) by FUZZY_1:40 .= (min (f,(UMF C))) . x by FUZZY_1:5 ; hence ( x in C implies (min (f,(1_minus g))) . x = f . x ) by FUZZY_1:18; ::_thesis: verum end; end; end; C = dom (min (f,(1_minus g))) by FUNCT_2:def_1; hence f \ g = f by A1, A3, PARTFUN1:5; ::_thesis: verum end; begin definition let C be non empty set ; let h, g be Membership_Func of C; funch * g -> Membership_Func of C means :Def2: :: FUZZY_2:def 2 for c being Element of C holds it . c = (h . c) * (g . c); existence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = (h . c) * (g . c) proof defpred S1[ set , set ] means \$2 = (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 = (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 = (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; 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 A15: 0 <= h . x by A8, A12, INTEGRA2:1; A16: 1 = upper_bound A by A11, INTEGRA1:5; x in dom g by A13, FUNCT_2:def_1; then A17: g . x in rng g by FUNCT_1:def_3; then A18: g . x <= 1 by A7, A16, INTEGRA2:1; 0 <= g . x by A7, A12, A17, INTEGRA2:1; then 0 <= (h . x) * (g . x) by A15, XREAL_1:127; then A19: 0 <= IT . x by A3, A9; h . x <= 1 by A8, A16, A14, INTEGRA2:1; then (h . x) * (g . x) <= 1 by A15, A18, XREAL_1:160; then IT . x <= 1 by A3, A9; hence y in [.0,1.] by A10, A12, A16, A19, INTEGRA2:1; ::_thesis: verum end; then rng IT c= [.0,1.] by TARSKI:def_3; then IT is Membership_Func of C by A5, FUNCT_2:def_1, RELAT_1:def_19; hence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = (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 = (h . c) * (g . c) ) & ( for c being Element of C holds b2 . c = (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 = (h . c) * (g . c) ) & ( for c being Element of C holds G . c = (h . c) * (g . c) ) implies F = G ) assume that A20: for c being Element of C holds F . c = (h . c) * (g . c) and A21: for c being Element of C holds G . c = (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 = (h . c) * (g . c) by A20; hence ( c in C implies F . c = G . c ) by A21; ::_thesis: verum end; A23: C = dom G by FUNCT_2:def_1; C = dom F by FUNCT_2:def_1; hence F = G by A23, A22, PARTFUN1:5; ::_thesis: verum end; commutativity for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = (h . c) * (g . c) ) holds for c being Element of C holds b1 . c = (g . c) * (h . c) ; end; :: deftheorem Def2 defines * FUZZY_2:def_2_:_ for C being non empty set for h, g, b4 being Membership_Func of C holds ( b4 = h * g iff for c being Element of C holds b4 . c = (h . c) * (g . c) ); definition let C be non empty set ; let h, g be Membership_Func of C; funch ++ g -> Membership_Func of C means :Def3: :: FUZZY_2:def 3 for c being Element of C holds it . c = ((h . c) + (g . c)) - ((h . c) * (g . c)); existence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) proof defpred S1[ set , set ] means \$2 = ((h . \$1) + (g . \$1)) - ((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 = ((h . x) + (g . x)) - ((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 = ((h . c) + (g . c)) - ((h . c) * (g . c)) by A3; 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 A7: x in dom IT and A8: y = IT . x by PARTFUN1:3; 0 <= (1_minus h) . x by Th1; then A9: 0 <= 1 - (h . x) by FUZZY_1:def_5; (1_minus g) . x <= 1 by Th1; then A10: 1 - (g . x) <= 1 by FUZZY_1:def_5; (1_minus h) . x <= 1 by Th1; then 1 - (h . x) <= 1 by FUZZY_1:def_5; then (1 - (h . x)) * (1 - (g . x)) <= 1 by A9, A10, XREAL_1:160; then 1 - ((1 - (h . x)) * (1 - (g . x))) >= 1 - 1 by XREAL_1:10; then 0 <= ((h . x) + (g . x)) - ((h . x) * (g . x)) ; then A11: 0 <= IT . x by A3, A7; A12: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A13: 1 = upper_bound A by INTEGRA1:5; 0 <= (1_minus g) . x by Th1; then 0 <= 1 - (g . x) by FUZZY_1:def_5; then 0 <= (1 - (h . x)) * (1 - (g . x)) by A9, XREAL_1:127; then 1 - 0 >= 1 - ((1 - (h . x)) * (1 - (g . x))) by XREAL_1:10; then ((h . x) + (g . x)) - ((h . x) * (g . x)) <= 1 ; then A14: IT . x <= 1 by A3, A7; 0 = lower_bound A by A12, INTEGRA1:5; hence y in [.0,1.] by A8, A13, A11, A14, INTEGRA2:1; ::_thesis: verum end; then rng IT c= [.0,1.] by TARSKI:def_3; then IT is Membership_Func of C by A5, FUNCT_2:def_1, RELAT_1:def_19; hence ex b1 being Membership_Func of C st for c being Element of C holds b1 . c = ((h . c) + (g . c)) - ((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 = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) & ( for c being Element of C holds b2 . c = ((h . c) + (g . c)) - ((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 = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) & ( for c being Element of C holds G . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) implies F = G ) assume that A15: for c being Element of C holds F . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) and A16: for c being Element of C holds G . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ; ::_thesis: F = G A17: 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 = ((h . c) + (g . c)) - ((h . c) * (g . c)) by A15; hence ( c in C implies F . c = G . c ) by A16; ::_thesis: verum end; A18: C = dom G by FUNCT_2:def_1; C = dom F by FUNCT_2:def_1; hence F = G by A18, A17, PARTFUN1:5; ::_thesis: verum end; commutativity for b1, h, g being Membership_Func of C st ( for c being Element of C holds b1 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) holds for c being Element of C holds b1 . c = ((g . c) + (h . c)) - ((g . c) * (h . c)) ; end; :: deftheorem Def3 defines ++ FUZZY_2:def_3_:_ for C being non empty set for h, g, b4 being Membership_Func of C holds ( b4 = h ++ g iff for c being Element of C holds b4 . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ); theorem Th28: :: FUZZY_2:28 for C being non empty set for f being Membership_Func of C holds ( f c= & f ++ f c= ) proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds ( f c= & f ++ f c= ) let f be Membership_Func of C; ::_thesis: ( f c= & f ++ f c= ) thus f c= ::_thesis: f ++ f c= proof let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f * f) . c <= f . c A1: 0 <= f . c by Th1; f . c <= 1 by Th1; then (f . c) * (f . c) <= 1 * (f . c) by A1, XREAL_1:64; hence (f * f) . c <= f . c by Def2; ::_thesis: verum end; let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . c <= (f ++ f) . c A2: 0 <= f . c by Th1; 0 <= (1_minus f) . c by Th1; then 0 * (f . c) <= (f . c) * ((1_minus f) . c) by A2, XREAL_1:64; then 0 <= (f . c) * (1 - (f . c)) by FUZZY_1:def_5; then 0 + (f . c) <= ((f . c) - ((f . c) * (f . c))) + (f . c) by XREAL_1:6; then f . c <= ((f . c) + (f . c)) - ((f . c) * (f . c)) ; hence f . c <= (f ++ f) . c by Def3; ::_thesis: verum end; theorem Th29: :: FUZZY_2:29 for C being non empty set for f, g, h being Membership_Func of C holds (f * g) * h = f * (g * h) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (f * g) * h = f * (g * h) let f, g, h be Membership_Func of C; ::_thesis: (f * g) * h = f * (g * h) A1: C = dom (f * (g * h)) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds ((f * g) * h) . c = (f * (g * h)) . c proof let c be Element of C; ::_thesis: ( c in C implies ((f * g) * h) . c = (f * (g * h)) . c ) ((f * g) * h) . c = ((f * g) . c) * (h . c) by Def2 .= ((f . c) * (g . c)) * (h . c) by Def2 .= (f . c) * ((g . c) * (h . c)) .= (f . c) * ((g * h) . c) by Def2 ; hence ( c in C implies ((f * g) * h) . c = (f * (g * h)) . c ) by Def2; ::_thesis: verum end; C = dom ((f * g) * h) by FUNCT_2:def_1; hence (f * g) * h = f * (g * h) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:30 for C being non empty set for f, g, h being Membership_Func of C holds (f ++ g) ++ h = f ++ (g ++ h) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (f ++ g) ++ h = f ++ (g ++ h) let f, g, h be Membership_Func of C; ::_thesis: (f ++ g) ++ h = f ++ (g ++ h) A1: C = dom (f ++ (g ++ h)) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds ((f ++ g) ++ h) . c = (f ++ (g ++ h)) . c proof let c be Element of C; ::_thesis: ( c in C implies ((f ++ g) ++ h) . c = (f ++ (g ++ h)) . c ) set x = f . c; set y = g . c; set z = h . c; A3: (f ++ (g ++ h)) . c = ((f . c) + ((g ++ h) . c)) - ((f . c) * ((g ++ h) . c)) by Def3 .= ((f . c) + (((g . c) + (h . c)) - ((g . c) * (h . c)))) - ((f . c) * ((g ++ h) . c)) by Def3 .= (((f . c) + ((g . c) + (h . c))) - ((g . c) * (h . c))) - ((f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c)))) by Def3 .= ((((- ((g . c) * (h . c))) - ((f . c) * (g . c))) - ((f . c) * (h . c))) + (((f . c) * (g . c)) * (h . c))) + (((f . c) + (g . c)) + (h . c)) ; ((f ++ g) ++ h) . c = (((f ++ g) . c) + (h . c)) - (((f ++ g) . c) * (h . c)) by Def3 .= ((((f . c) + (g . c)) - ((f . c) * (g . c))) + (h . c)) - (((f ++ g) . c) * (h . c)) by Def3 .= (((- ((f . c) * (g . c))) + ((f . c) + (g . c))) + (h . c)) - ((((f . c) + (g . c)) - ((f . c) * (g . c))) * (h . c)) by Def3 .= ((((- ((f . c) * (g . c))) - ((f . c) * (h . c))) - ((g . c) * (h . c))) + (((f . c) * (g . c)) * (h . c))) + (((f . c) + (g . c)) + (h . c)) ; hence ( c in C implies ((f ++ g) ++ h) . c = (f ++ (g ++ h)) . c ) by A3; ::_thesis: verum end; C = dom ((f ++ g) ++ h) by FUNCT_2:def_1; hence (f ++ g) ++ h = f ++ (g ++ h) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:31 for C being non empty set for f, g being Membership_Func of C holds ( f c= & f ++ (f * g) c= ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( f c= & f ++ (f * g) c= ) let f, g be Membership_Func of C; ::_thesis: ( f c= & f ++ (f * g) c= ) thus f c= ::_thesis: f ++ (f * g) c= proof let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f * (f ++ g)) . c <= f . c A1: (f ++ g) . c <= 1 by Th1; 0 <= f . c by Th1; then ((f ++ g) . c) * (f . c) <= 1 * (f . c) by A1, XREAL_1:64; hence (f * (f ++ g)) . c <= f . c by Def2; ::_thesis: verum end; let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: f . c <= (f ++ (f * g)) . c A2: (1_minus f) . c >= 0 by Th1; (f * g) . c >= 0 by Th1; then 0 * ((f * g) . c) <= ((1_minus f) . c) * ((f * g) . c) by A2, XREAL_1:64; then 0 <= (1 - (f . c)) * ((f * g) . c) by FUZZY_1:def_5; then 0 + (f . c) <= (((f * g) . c) - ((f . c) * ((f * g) . c))) + (f . c) by XREAL_1:6; then f . c <= ((f . c) + ((f * g) . c)) - ((f . c) * ((f * g) . c)) ; hence f . c <= (f ++ (f * g)) . c by Def3; ::_thesis: verum end; theorem :: FUZZY_2:32 for C being non empty set for f, g, h being Membership_Func of C holds (f * g) ++ (f * h) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (f * g) ++ (f * h) c= let f, g, h be Membership_Func of C; ::_thesis: (f * g) ++ (f * h) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f * (g ++ h)) . c <= ((f * g) ++ (f * h)) . c set x = f . c; set y = g . c; set z = h . c; f c= by Th28; then A1: (f * f) . c <= f . c by FUZZY_1:def_2; (g * h) . c >= 0 by Th1; then ((f * f) . c) * ((g * h) . c) <= (f . c) * ((g * h) . c) by A1, XREAL_1:64; then (((f * g) . c) + ((f * h) . c)) - (((f * f) . c) * ((g * h) . c)) >= (((f * g) . c) + ((f * h) . c)) - ((f . c) * ((g * h) . c)) by XREAL_1:10; then (((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c) >= (((f * g) . c) + ((f * h) . c)) - ((f . c) * ((g * h) . c)) by Def2; then (((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c) >= (((f . c) * (g . c)) + ((f * h) . c)) - ((f . c) * ((g * h) . c)) by Def2; then (((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c) >= (((f . c) * (g . c)) + ((f . c) * (h . c))) - ((f . c) * ((g * h) . c)) by Def2; then (((f * g) . c) + ((f * h) . c)) - ((f * (f * (g * h))) . c) >= (((f . c) * (g . c)) + ((f . c) * (h . c))) - ((f . c) * ((g * h) . c)) by Th29; then (((f * g) . c) + ((f * h) . c)) - ((f * ((g * f) * h)) . c) >= (((g . c) + (h . c)) - ((g * h) . c)) * (f . c) by Th29; then (((f * g) . c) + ((f * h) . c)) - (((f * g) * (f * h)) . c) >= (((g . c) + (h . c)) - ((g * h) . c)) * (f . c) by Th29; then (((f * g) . c) + ((f * h) . c)) - (((f * g) * (f * h)) . c) >= (f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c))) by Def2; then (((f * g) . c) + ((f * h) . c)) - (((f * g) . c) * ((f * h) . c)) >= (f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c))) by Def2; then ((f * g) ++ (f * h)) . c >= (f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c))) by Def3; then ((f * g) ++ (f * h)) . c >= (f . c) * ((g ++ h) . c) by Def3; hence (f * (g ++ h)) . c <= ((f * g) ++ (f * h)) . c by Def2; ::_thesis: verum end; theorem :: FUZZY_2:33 for C being non empty set for f, g, h being Membership_Func of C holds f ++ (g * h) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f ++ (g * h) c= let f, g, h be Membership_Func of C; ::_thesis: f ++ (g * h) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: ((f ++ g) * (f ++ h)) . c <= (f ++ (g * h)) . c set x = f . c; set y = g . c; set z = h . c; f c= by Th28; then (f * f) . c <= f . c by FUZZY_1:def_2; then (f . c) * (f . c) <= f . c by Def2; then A1: ((f . c) * (f . c)) - (f . c) <= 0 by XREAL_1:47; 0 <= (1_minus (g ++ h)) . c by Th1; then A2: ((1_minus (g ++ h)) . c) * ((- (f . c)) + ((f . c) * (f . c))) <= 0 * ((- (f . c)) + ((f . c) * (f . c))) by A1, XREAL_1:65; (((f ++ g) * (f ++ h)) . c) - ((f ++ (g * h)) . c) = (((f ++ g) . c) * ((f ++ h) . c)) - ((f ++ (g * h)) . c) by Def2 .= ((((f . c) + (g . c)) - ((f . c) * (g . c))) * ((f ++ h) . c)) - ((f ++ (g * h)) . c) by Def3 .= ((((f . c) + (g . c)) - ((f . c) * (g . c))) * (((f . c) + (h . c)) - ((f . c) * (h . c)))) - ((f ++ (g * h)) . c) by Def3 .= ((((f . c) + (g . c)) - ((f . c) * (g . c))) * (((f . c) + (h . c)) - ((f . c) * (h . c)))) - (((f . c) + ((g * h) . c)) - ((f . c) * ((g * h) . c))) by Def3 .= ((((f . c) + (g . c)) - ((f . c) * (g . c))) * (((f . c) + (h . c)) - ((f . c) * (h . c)))) - (((f . c) + ((g . c) * (h . c))) - ((f . c) * ((g * h) . c))) by Def2 .= ((((f . c) - ((f . c) * (g . c))) + (g . c)) * (((f . c) + (h . c)) - ((f . c) * (h . c)))) - (((f . c) + ((g . c) * (h . c))) - (((g . c) * (h . c)) * (f . c))) by Def2 .= ((f . c) * ((((g . c) + (h . c)) - ((g . c) * (h . c))) - 1)) + (((((- (g . c)) + ((g . c) * (h . c))) - (h . c)) + 1) * ((f . c) * (f . c))) .= ((f . c) * (((g ++ h) . c) - 1)) + (((- (((g . c) + (h . c)) - ((g . c) * (h . c)))) + 1) * ((f . c) * (f . c))) by Def3 .= ((f . c) * (- ((- ((g ++ h) . c)) + 1))) + (((- ((g ++ h) . c)) + 1) * ((f . c) * (f . c))) by Def3 .= (1 - ((g ++ h) . c)) * ((- (f . c)) + ((f . c) * (f . c))) .= ((1_minus (g ++ h)) . c) * ((- (f . c)) + ((f . c) * (f . c))) by FUZZY_1:def_5 ; hence ((f ++ g) * (f ++ h)) . c <= (f ++ (g * h)) . c by A2, XREAL_1:50; ::_thesis: verum end; theorem :: FUZZY_2:34 for C being non empty set for f, g being Membership_Func of C holds 1_minus (f * g) = (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 (f * g) = (1_minus f) ++ (1_minus g) let f, g be Membership_Func of C; ::_thesis: 1_minus (f * g) = (1_minus f) ++ (1_minus g) A1: C = dom ((1_minus f) ++ (1_minus g)) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (1_minus (f * g)) . c = ((1_minus f) ++ (1_minus g)) . c proof let c be Element of C; ::_thesis: ( c in C implies (1_minus (f * g)) . c = ((1_minus f) ++ (1_minus g)) . c ) ((1_minus f) ++ (1_minus g)) . c = (((1_minus f) . c) + ((1_minus g) . c)) - (((1_minus f) . c) * ((1_minus g) . c)) by Def3 .= ((1 - (f . c)) + ((1_minus g) . c)) - (((1_minus f) . c) * ((1_minus g) . c)) by FUZZY_1:def_5 .= ((1 - (f . c)) + (1 - (g . c))) - (((1_minus f) . c) * ((1_minus g) . c)) by FUZZY_1:def_5 .= ((1 - (f . c)) + (1 - (g . c))) - ((1 - (f . c)) * ((1_minus g) . c)) by FUZZY_1:def_5 .= ((1 - (f . c)) + (1 - (g . c))) - ((1 - (f . c)) * (1 - (g . c))) by FUZZY_1:def_5 .= (((g . c) - (g . c)) + 1) - ((f . c) * (g . c)) .= 1 - ((f * g) . c) by Def2 ; hence ( c in C implies (1_minus (f * g)) . c = ((1_minus f) ++ (1_minus g)) . c ) by FUZZY_1:def_5; ::_thesis: verum end; C = dom (1_minus (f * g)) by FUNCT_2:def_1; hence 1_minus (f * g) = (1_minus f) ++ (1_minus g) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:35 for C being non empty set for f, g being Membership_Func of C holds 1_minus (f ++ g) = (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 (f ++ g) = (1_minus f) * (1_minus g) let f, g be Membership_Func of C; ::_thesis: 1_minus (f ++ g) = (1_minus f) * (1_minus g) A1: C = dom ((1_minus f) * (1_minus g)) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (1_minus (f ++ g)) . c = ((1_minus f) * (1_minus g)) . c proof let c be Element of C; ::_thesis: ( c in C implies (1_minus (f ++ g)) . c = ((1_minus f) * (1_minus g)) . c ) ((1_minus f) * (1_minus g)) . c = ((1_minus f) . c) * ((1_minus g) . c) by Def2 .= (1 - (f . c)) * ((1_minus g) . c) by FUZZY_1:def_5 .= (1 - (f . c)) * (1 - (g . c)) by FUZZY_1:def_5 .= 1 - (((f . c) + (g . c)) - ((f . c) * (g . c))) .= 1 - ((f ++ g) . c) by Def3 ; hence ( c in C implies (1_minus (f ++ g)) . c = ((1_minus f) * (1_minus g)) . c ) by FUZZY_1:def_5; ::_thesis: verum end; C = dom (1_minus (f ++ g)) by FUNCT_2:def_1; hence 1_minus (f ++ g) = (1_minus f) * (1_minus g) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem Th36: :: FUZZY_2:36 for C being non empty set for f, g being Membership_Func of C holds f ++ g = 1_minus ((1_minus f) * (1_minus g)) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds f ++ g = 1_minus ((1_minus f) * (1_minus g)) let f, g be Membership_Func of C; ::_thesis: f ++ g = 1_minus ((1_minus f) * (1_minus g)) A1: C = dom (1_minus ((1_minus f) * (1_minus g))) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (f ++ g) . c = (1_minus ((1_minus f) * (1_minus g))) . c proof let c be Element of C; ::_thesis: ( c in C implies (f ++ g) . c = (1_minus ((1_minus f) * (1_minus g))) . c ) (1_minus ((1_minus f) * (1_minus g))) . c = 1 - (((1_minus f) * (1_minus g)) . c) by FUZZY_1:def_5 .= 1 - (((1_minus f) . c) * ((1_minus g) . c)) by Def2 .= 1 - ((1 - (f . c)) * ((1_minus g) . c)) by FUZZY_1:def_5 .= 1 - ((1 - (f . c)) * (1 - (g . c))) by FUZZY_1:def_5 .= ((f . c) + (g . c)) - ((f . c) * (g . c)) ; hence ( c in C implies (f ++ g) . c = (1_minus ((1_minus f) * (1_minus g))) . c ) by Def3; ::_thesis: verum end; C = dom (f ++ g) by FUNCT_2:def_1; hence f ++ g = 1_minus ((1_minus f) * (1_minus g)) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:37 for C being non empty set for f being Membership_Func of C holds ( f * (EMF C) = EMF C & f * (UMF C) = f ) proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds ( f * (EMF C) = EMF C & f * (UMF C) = f ) let f be Membership_Func of C; ::_thesis: ( f * (EMF C) = EMF C & f * (UMF C) = f ) A1: C = dom (f * (EMF C)) by FUNCT_2:def_1; A2: C = dom f by FUNCT_2:def_1; A3: for c being Element of C st c in C holds (f * (UMF C)) . c = f . c proof let c be Element of C; ::_thesis: ( c in C implies (f * (UMF C)) . c = f . c ) (f * (UMF C)) . c = (f . c) * ((UMF C) . c) by Def2 .= (f . c) * 1 by FUNCT_3:def_3 ; hence ( c in C implies (f * (UMF C)) . c = f . c ) ; ::_thesis: verum end; A4: for c being Element of C st c in C holds (f * (EMF C)) . c = (EMF C) . c proof let c be Element of C; ::_thesis: ( c in C implies (f * (EMF C)) . c = (EMF C) . c ) (f * (EMF C)) . c = (f . c) * ((EMF C) . c) by Def2 .= (f . c) * 0 by FUNCT_3:def_3 ; hence ( c in C implies (f * (EMF C)) . c = (EMF C) . c ) by FUNCT_3:def_3; ::_thesis: verum end; A5: C = dom (f * (UMF C)) by FUNCT_2:def_1; C = dom (EMF C) by FUNCT_2:def_1; hence ( f * (EMF C) = EMF C & f * (UMF C) = f ) by A1, A4, A2, A5, A3, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:38 for C being non empty set for f being Membership_Func of C holds ( f ++ (EMF C) = f & f ++ (UMF C) = UMF C ) proof let C be non empty set ; ::_thesis: for f being Membership_Func of C holds ( f ++ (EMF C) = f & f ++ (UMF C) = UMF C ) let f be Membership_Func of C; ::_thesis: ( f ++ (EMF C) = f & f ++ (UMF C) = UMF C ) A1: C = dom (f ++ (EMF C)) by FUNCT_2:def_1; A2: C = dom (UMF C) by FUNCT_2:def_1; A3: for c being Element of C st c in C holds (f ++ (UMF C)) . c = (UMF C) . c proof let c be Element of C; ::_thesis: ( c in C implies (f ++ (UMF C)) . c = (UMF C) . c ) (f ++ (UMF C)) . c = ((f . c) + ((UMF C) . c)) - ((f . c) * ((UMF C) . c)) by Def3 .= (((UMF C) . c) + (f . c)) - ((f . c) * 1) by FUNCT_3:def_3 .= ((UMF C) . c) + ((f . c) - (f . c)) ; hence ( c in C implies (f ++ (UMF C)) . c = (UMF C) . c ) ; ::_thesis: verum end; A4: for c being Element of C st c in C holds (f ++ (EMF C)) . c = f . c proof let c be Element of C; ::_thesis: ( c in C implies (f ++ (EMF C)) . c = f . c ) (f ++ (EMF C)) . c = ((f . c) + ((EMF C) . c)) - ((f . c) * ((EMF C) . c)) by Def3 .= ((f . c) + 0) - ((f . c) * ((EMF C) . c)) by FUNCT_3:def_3 .= (f . c) - ((f . c) * 0) by FUNCT_3:def_3 ; hence ( c in C implies (f ++ (EMF C)) . c = f . c ) ; ::_thesis: verum end; A5: C = dom (f ++ (UMF C)) by FUNCT_2:def_1; C = dom f by FUNCT_2:def_1; hence ( f ++ (EMF C) = f & f ++ (UMF C) = UMF C ) by A1, A4, A2, A5, A3, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:39 for C being non empty set for f, g being Membership_Func of C holds min (f,g) c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds min (f,g) c= let f, g be Membership_Func of C; ::_thesis: min (f,g) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (f * g) . c <= (min (f,g)) . c A1: (min (f,g)) . c = min ((f . c),(g . c)) by FUZZY_1:5; percases ( (min (f,g)) . c = f . c or (min (f,g)) . c = g . c ) by A1, XXREAL_0:15; supposeA2: (min (f,g)) . c = f . c ; ::_thesis: (f * g) . c <= (min (f,g)) . c A3: f . c >= 0 by Th1; g . c <= 1 by Th1; then (g . c) * (f . c) <= 1 * (f . c) by A3, XREAL_1:64; hence (f * g) . c <= (min (f,g)) . c by A2, Def2; ::_thesis: verum end; supposeA4: (min (f,g)) . c = g . c ; ::_thesis: (f * g) . c <= (min (f,g)) . c A5: g . c >= 0 by Th1; f . c <= 1 by Th1; then (f . c) * (g . c) <= 1 * (g . c) by A5, XREAL_1:64; hence (f * g) . c <= (min (f,g)) . c by A4, Def2; ::_thesis: verum end; end; end; theorem :: FUZZY_2:40 for C being non empty set for f, g being Membership_Func of C holds f ++ g c= proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds f ++ g c= let f, g be Membership_Func of C; ::_thesis: f ++ g c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,g)) . c <= (f ++ g) . c A1: (max (f,g)) . c = max ((f . c),(g . c)) by FUZZY_1:5; percases ( (max (f,g)) . c = f . c or (max (f,g)) . c = g . c ) by A1, XXREAL_0:16; supposeA2: (max (f,g)) . c = f . c ; ::_thesis: (max (f,g)) . c <= (f ++ g) . c A3: (1_minus f) . c >= 0 by Th1; g . c >= 0 by Th1; then 0 * (g . c) <= (g . c) * ((1_minus f) . c) by A3, XREAL_1:64; then 0 <= (g . c) * (1 - (f . c)) by FUZZY_1:def_5; then 0 + (f . c) <= ((g . c) - ((f . c) * (g . c))) + (f . c) by XREAL_1:6; then f . c <= ((f . c) + (g . c)) - ((f . c) * (g . c)) ; hence (max (f,g)) . c <= (f ++ g) . c by A2, Def3; ::_thesis: verum end; supposeA4: (max (f,g)) . c = g . c ; ::_thesis: (max (f,g)) . c <= (f ++ g) . c A5: (1_minus g) . c >= 0 by Th1; f . c >= 0 by Th1; then 0 * (f . c) <= (f . c) * ((1_minus g) . c) by A5, XREAL_1:64; then 0 <= (f . c) * (1 - (g . c)) by FUZZY_1:def_5; then 0 + (g . c) <= ((f . c) - ((f . c) * (g . c))) + (g . c) by XREAL_1:6; then g . c <= ((f . c) + (g . c)) - ((f . c) * (g . c)) ; hence (max (f,g)) . c <= (f ++ g) . c by A4, Def3; ::_thesis: verum end; end; end; Lm1: for a, b, c being Real st 0 <= c holds c * (min (a,b)) = min ((c * a),(c * b)) proof let a, b, c be Element of REAL ; ::_thesis: ( 0 <= c implies c * (min (a,b)) = min ((c * a),(c * b)) ) assume A1: 0 <= c ; ::_thesis: c * (min (a,b)) = min ((c * a),(c * b)) percases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15; supposeA2: min (a,b) = a ; ::_thesis: c * (min (a,b)) = min ((c * a),(c * b)) then a <= b by XXREAL_0:def_9; then a * c <= b * c by A1, XREAL_1:64; hence c * (min (a,b)) = min ((c * a),(c * b)) by A2, XXREAL_0:def_9; ::_thesis: verum end; supposeA3: min (a,b) = b ; ::_thesis: c * (min (a,b)) = min ((c * a),(c * b)) then a >= b by XXREAL_0:def_9; then a * c >= b * c by A1, XREAL_1:64; hence c * (min (a,b)) = min ((c * a),(c * b)) by A3, XXREAL_0:def_9; ::_thesis: verum end; end; end; Lm2: for a, b, c being Real st 0 <= c holds c * (max (a,b)) = max ((c * a),(c * b)) proof let a, b, c be Element of REAL ; ::_thesis: ( 0 <= c implies c * (max (a,b)) = max ((c * a),(c * b)) ) assume A1: 0 <= c ; ::_thesis: c * (max (a,b)) = max ((c * a),(c * b)) percases ( max (a,b) = b or max (a,b) = a ) by XXREAL_0:16; supposeA2: max (a,b) = b ; ::_thesis: c * (max (a,b)) = max ((c * a),(c * b)) then a <= b by XXREAL_0:def_10; then a * c <= c * b by A1, XREAL_1:64; hence c * (max (a,b)) = max ((c * a),(c * b)) by A2, XXREAL_0:def_10; ::_thesis: verum end; supposeA3: max (a,b) = a ; ::_thesis: c * (max (a,b)) = max ((c * a),(c * b)) then a >= b by XXREAL_0:def_10; then a * c >= b * c by A1, XREAL_1:64; hence c * (max (a,b)) = max ((c * a),(c * b)) by A3, XXREAL_0:def_10; ::_thesis: verum end; end; end; theorem :: FUZZY_2:41 for a, b, c being Real st 0 <= c holds ( c * (max (a,b)) = max ((c * a),(c * b)) & c * (min (a,b)) = min ((c * a),(c * b)) ) by Lm1, Lm2; theorem :: FUZZY_2:42 for a, b, c being Real holds ( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) ) proof let a, b, c be Element of REAL ; ::_thesis: ( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) ) A1: c + (min (a,b)) = min ((c + a),(c + b)) proof percases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15; supposeA2: min (a,b) = a ; ::_thesis: c + (min (a,b)) = min ((c + a),(c + b)) then a <= b by XXREAL_0:def_9; then a + c <= c + b by XREAL_1:6; hence c + (min (a,b)) = min ((c + a),(c + b)) by A2, XXREAL_0:def_9; ::_thesis: verum end; supposeA3: min (a,b) = b ; ::_thesis: c + (min (a,b)) = min ((c + a),(c + b)) then a >= b by XXREAL_0:def_9; then a + c >= b + c by XREAL_1:6; hence c + (min (a,b)) = min ((c + a),(c + b)) by A3, XXREAL_0:def_9; ::_thesis: verum end; end; end; c + (max (a,b)) = max ((c + a),(c + b)) proof percases ( max (a,b) = b or max (a,b) = a ) by XXREAL_0:16; supposeA4: max (a,b) = b ; ::_thesis: c + (max (a,b)) = max ((c + a),(c + b)) then a <= b by XXREAL_0:def_10; then c + a <= c + b by XREAL_1:6; hence c + (max (a,b)) = max ((c + a),(c + b)) by A4, XXREAL_0:def_10; ::_thesis: verum end; supposeA5: max (a,b) = a ; ::_thesis: c + (max (a,b)) = max ((c + a),(c + b)) then a >= b by XXREAL_0:def_10; then a + c >= b + c by XREAL_1:6; hence c + (max (a,b)) = max ((c + a),(c + b)) by A5, XXREAL_0:def_10; ::_thesis: verum end; end; end; hence ( c + (max (a,b)) = max ((c + a),(c + b)) & c + (min (a,b)) = min ((c + a),(c + b)) ) by A1; ::_thesis: verum end; theorem :: FUZZY_2:43 for C being non empty set for f, g, h being Membership_Func of C holds f * (max (g,h)) = max ((f * g),(f * h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f * (max (g,h)) = max ((f * g),(f * h)) let f, g, h be Membership_Func of C; ::_thesis: f * (max (g,h)) = max ((f * g),(f * h)) A1: C = dom (max ((f * g),(f * h))) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (f * (max (g,h))) . c = (max ((f * g),(f * h))) . c proof let c be Element of C; ::_thesis: ( c in C implies (f * (max (g,h))) . c = (max ((f * g),(f * h))) . c ) (f * (max (g,h))) . c = (f . c) * ((max (g,h)) . c) by Def2 .= (f . c) * (max ((g . c),(h . c))) by FUZZY_1:5 .= max (((f . c) * (g . c)),((f . c) * (h . c))) by Lm2, Th1 .= max (((f * g) . c),((f . c) * (h . c))) by Def2 .= max (((f * g) . c),((f * h) . c)) by Def2 ; hence ( c in C implies (f * (max (g,h))) . c = (max ((f * g),(f * h))) . c ) by FUZZY_1:5; ::_thesis: verum end; C = dom (f * (max (g,h))) by FUNCT_2:def_1; hence f * (max (g,h)) = max ((f * g),(f * h)) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:44 for C being non empty set for f, g, h being Membership_Func of C holds f * (min (g,h)) = min ((f * g),(f * h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f * (min (g,h)) = min ((f * g),(f * h)) let f, g, h be Membership_Func of C; ::_thesis: f * (min (g,h)) = min ((f * g),(f * h)) A1: C = dom (min ((f * g),(f * h))) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (f * (min (g,h))) . c = (min ((f * g),(f * h))) . c proof let c be Element of C; ::_thesis: ( c in C implies (f * (min (g,h))) . c = (min ((f * g),(f * h))) . c ) (f * (min (g,h))) . c = (f . c) * ((min (g,h)) . c) by Def2 .= (f . c) * (min ((g . c),(h . c))) by FUZZY_1:5 .= min (((f . c) * (g . c)),((f . c) * (h . c))) by Lm1, Th1 .= min (((f * g) . c),((f . c) * (h . c))) by Def2 .= min (((f * g) . c),((f * h) . c)) by Def2 ; hence ( c in C implies (f * (min (g,h))) . c = (min ((f * g),(f * h))) . c ) by FUZZY_1:5; ::_thesis: verum end; C = dom (f * (min (g,h))) by FUNCT_2:def_1; hence f * (min (g,h)) = min ((f * g),(f * h)) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:45 for C being non empty set for f, g, h being Membership_Func of C holds f ++ (max (g,h)) = max ((f ++ g),(f ++ h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f ++ (max (g,h)) = max ((f ++ g),(f ++ h)) let f, g, h be Membership_Func of C; ::_thesis: f ++ (max (g,h)) = max ((f ++ g),(f ++ h)) A1: C = dom (max ((f ++ g),(f ++ h))) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (f ++ (max (g,h))) . c = (max ((f ++ g),(f ++ h))) . c proof let c be Element of C; ::_thesis: ( c in C implies (f ++ (max (g,h))) . c = (max ((f ++ g),(f ++ h))) . c ) A3: (f ++ (max (g,h))) . c = ((f . c) + ((max (g,h)) . c)) - ((f . c) * ((max (g,h)) . c)) by Def3 .= ((f . c) + (max ((g . c),(h . c)))) - ((f . c) * ((max (g,h)) . c)) by FUZZY_1:5 ; percases ( max ((g . c),(h . c)) = g . c or max ((g . c),(h . c)) = h . c ) by XXREAL_0:16; supposeA4: max ((g . c),(h . c)) = g . c ; ::_thesis: ( c in C implies (f ++ (max (g,h))) . c = (max ((f ++ g),(f ++ h))) . c ) A5: (1_minus f) . c >= 0 by Th1; g . c >= h . c by A4, XXREAL_0:def_10; then (g . c) * ((1_minus f) . c) >= (h . c) * ((1_minus f) . c) by A5, XREAL_1:64; then (g . c) * (1 - (f . c)) >= (h . c) * ((1_minus f) . c) by FUZZY_1:def_5; then (g . c) * (1 - (f . c)) >= (h . c) * (1 - (f . c)) by FUZZY_1:def_5; then (((g . c) * 1) - ((g . c) * (f . c))) + (f . c) >= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; then A6: ((f . c) + (g . c)) - ((f . c) * (g . c)) = max ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by XXREAL_0:def_10 .= max (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by Def3 .= max (((f ++ g) . c),((f ++ h) . c)) by Def3 ; (f ++ (max (g,h))) . c = ((f . c) + (g . c)) - ((f . c) * (g . c)) by A3, A4, FUZZY_1:5; hence ( c in C implies (f ++ (max (g,h))) . c = (max ((f ++ g),(f ++ h))) . c ) by A6, FUZZY_1:5; ::_thesis: verum end; supposeA7: max ((g . c),(h . c)) = h . c ; ::_thesis: ( c in C implies (f ++ (max (g,h))) . c = (max ((f ++ g),(f ++ h))) . c ) A8: (1_minus f) . c >= 0 by Th1; h . c >= g . c by A7, XXREAL_0:def_10; then (h . c) * ((1_minus f) . c) >= (g . c) * ((1_minus f) . c) by A8, XREAL_1:64; then (h . c) * (1 - (f . c)) >= (g . c) * ((1_minus f) . c) by FUZZY_1:def_5; then (h . c) * (1 - (f . c)) >= (g . c) * (1 - (f . c)) by FUZZY_1:def_5; then (((h . c) * 1) - ((h . c) * (f . c))) + (f . c) >= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; then A9: ((f . c) + (h . c)) - ((f . c) * (h . c)) = max ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by XXREAL_0:def_10 .= max (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by Def3 .= max (((f ++ g) . c),((f ++ h) . c)) by Def3 ; (f ++ (max (g,h))) . c = ((f . c) + (h . c)) - ((f . c) * (h . c)) by A3, A7, FUZZY_1:5; hence ( c in C implies (f ++ (max (g,h))) . c = (max ((f ++ g),(f ++ h))) . c ) by A9, FUZZY_1:5; ::_thesis: verum end; end; end; C = dom (f ++ (max (g,h))) by FUNCT_2:def_1; hence f ++ (max (g,h)) = max ((f ++ g),(f ++ h)) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:46 for C being non empty set for f, g, h being Membership_Func of C holds f ++ (min (g,h)) = min ((f ++ g),(f ++ h)) proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds f ++ (min (g,h)) = min ((f ++ g),(f ++ h)) let f, g, h be Membership_Func of C; ::_thesis: f ++ (min (g,h)) = min ((f ++ g),(f ++ h)) A1: C = dom (min ((f ++ g),(f ++ h))) by FUNCT_2:def_1; A2: for c being Element of C st c in C holds (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c proof let c be Element of C; ::_thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) A3: (f ++ (min (g,h))) . c = ((f . c) + ((min (g,h)) . c)) - ((f . c) * ((min (g,h)) . c)) by Def3 .= ((f . c) + (min ((g . c),(h . c)))) - ((f . c) * ((min (g,h)) . c)) by FUZZY_1:5 ; now__::_thesis:_(_c_in_C_implies_(f_++_(min_(g,h)))_._c_=_(min_((f_++_g),(f_++_h)))_._c_) percases ( min ((g . c),(h . c)) = g . c or min ((g . c),(h . c)) = h . c ) by XXREAL_0:15; supposeA4: min ((g . c),(h . c)) = g . c ; ::_thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) A5: (1_minus f) . c >= 0 by Th1; g . c <= h . c by A4, XXREAL_0:def_9; then (g . c) * ((1_minus f) . c) <= (h . c) * ((1_minus f) . c) by A5, XREAL_1:64; then (g . c) * (1 - (f . c)) <= (h . c) * ((1_minus f) . c) by FUZZY_1:def_5; then (g . c) * (1 - (f . c)) <= (h . c) * (1 - (f . c)) by FUZZY_1:def_5; then (((g . c) * 1) - ((g . c) * (f . c))) + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; then A6: ((f . c) + (g . c)) - ((f . c) * (g . c)) = min ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by XXREAL_0:def_9 .= min (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by Def3 .= min (((f ++ g) . c),((f ++ h) . c)) by Def3 ; (f ++ (min (g,h))) . c = ((f . c) + (g . c)) - ((f . c) * (g . c)) by A3, A4, FUZZY_1:5; hence ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) by A6, FUZZY_1:5; ::_thesis: verum end; supposeA7: min ((g . c),(h . c)) = h . c ; ::_thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) A8: (1_minus f) . c >= 0 by Th1; h . c <= g . c by A7, XXREAL_0:def_9; then (h . c) * ((1_minus f) . c) <= (g . c) * ((1_minus f) . c) by A8, XREAL_1:64; then (h . c) * (1 - (f . c)) <= (g . c) * ((1_minus f) . c) by FUZZY_1:def_5; then (h . c) * (1 - (f . c)) <= (g . c) * (1 - (f . c)) by FUZZY_1:def_5; then (((h . c) * 1) - ((h . c) * (f . c))) + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; then A9: ((f . c) + (h . c)) - ((f . c) * (h . c)) = min ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by XXREAL_0:def_9 .= min (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by Def3 .= min (((f ++ g) . c),((f ++ h) . c)) by Def3 ; (f ++ (min (g,h))) . c = ((f . c) + (h . c)) - ((f . c) * (h . c)) by A3, A7, FUZZY_1:5; hence ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) by A9, FUZZY_1:5; ::_thesis: verum end; end; end; hence ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) ; ::_thesis: verum end; C = dom (f ++ (min (g,h))) by FUNCT_2:def_1; hence f ++ (min (g,h)) = min ((f ++ g),(f ++ h)) by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem :: FUZZY_2:47 for C being non empty set for f, g, h being Membership_Func of C holds max (f,(g * h)) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds max (f,(g * h)) c= let f, g, h be Membership_Func of C; ::_thesis: max (f,(g * h)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: ((max (f,g)) * (max (f,h))) . c <= (max (f,(g * h))) . c A1: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c proof percases ( max ((f . c),(g . c)) = f . c or max ((f . c),(g . c)) = g . c ) by XXREAL_0:16; supposeA2: max ((f . c),(g . c)) = f . c ; ::_thesis: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c proof percases ( max ((f . c),(h . c)) = f . c or max ((f . c),(h . c)) = h . c ) by XXREAL_0:16; supposeA3: max ((f . c),(h . c)) = f . c ; ::_thesis: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c (max (f,(g * h))) . c = max ((f . c),((g * h) . c)) by FUZZY_1:5; then A4: (max (f,(g * h))) . c >= f . c by XXREAL_0:25; f c= by Th28; then (f * f) . c <= f . c by FUZZY_1:def_2; then (f * f) . c <= (max (f,(g * h))) . c by A4, XXREAL_0:2; hence (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c by A2, A3, Def2; ::_thesis: verum end; supposeA5: max ((f . c),(h . c)) = h . c ; ::_thesis: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c A6: 1 >= h . c by Th1; f . c <= max ((f . c),((g * h) . c)) by XXREAL_0:25; then A7: f . c <= (max (f,(g * h))) . c by FUZZY_1:5; f . c >= 0 by Th1; then (f . c) * (h . c) <= (f . c) * 1 by A6, XREAL_1:64; hence (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c by A2, A5, A7, XXREAL_0:2; ::_thesis: verum end; end; end; hence (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c ; ::_thesis: verum end; supposeA8: max ((f . c),(g . c)) = g . c ; ::_thesis: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c proof percases ( max ((f . c),(h . c)) = f . c or max ((f . c),(h . c)) = h . c ) by XXREAL_0:16; supposeA9: max ((f . c),(h . c)) = f . c ; ::_thesis: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c A10: 1 >= g . c by Th1; f . c <= max ((f . c),((g * h) . c)) by XXREAL_0:25; then A11: f . c <= (max (f,(g * h))) . c by FUZZY_1:5; f . c >= 0 by Th1; then (f . c) * (g . c) <= (f . c) * 1 by A10, XREAL_1:64; hence (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c by A8, A9, A11, XXREAL_0:2; ::_thesis: verum end; supposeA12: max ((f . c),(h . c)) = h . c ; ::_thesis: (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c (max (f,(g * h))) . c = max ((f . c),((g * h) . c)) by FUZZY_1:5; then (max (f,(g * h))) . c >= (g * h) . c by XXREAL_0:25; hence (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c by A8, A12, Def2; ::_thesis: verum end; end; end; hence (max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c ; ::_thesis: verum end; end; end; ((max (f,g)) * (max (f,h))) . c = ((max (f,g)) . c) * ((max (f,h)) . c) by Def2 .= (max ((f . c),(g . c))) * ((max (f,h)) . c) by FUZZY_1:5 .= (max ((f . c),(g . c))) * (max ((f . c),(h . c))) by FUZZY_1:5 ; hence ((max (f,g)) * (max (f,h))) . c <= (max (f,(g * h))) . c by A1; ::_thesis: verum end; theorem :: FUZZY_2:48 for C being non empty set for f, g, h being Membership_Func of C holds min (f,(g * h)) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds min (f,(g * h)) c= let f, g, h be Membership_Func of C; ::_thesis: min (f,(g * h)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: ((min (f,g)) * (min (f,h))) . c <= (min (f,(g * h))) . c A1: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c proof now__::_thesis:_(min_((f_._c),(g_._c)))_*_(min_((f_._c),(h_._c)))_<=_(min_(f,(g_*_h)))_._c percases ( min ((f . c),(g . c)) = f . c or min ((f . c),(g . c)) = g . c ) by XXREAL_0:15; supposeA2: min ((f . c),(g . c)) = f . c ; ::_thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c proof percases ( min ((f . c),(h . c)) = f . c or min ((f . c),(h . c)) = h . c ) by XXREAL_0:15; supposeA3: min ((f . c),(h . c)) = f . c ; ::_thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c A4: 0 <= g . c by Th1; f . c <= h . c by A3, XXREAL_0:def_9; then A5: (g . c) * (f . c) <= (h . c) * (g . c) by A4, XREAL_1:64; A6: 0 <= f . c by Th1; f c= by Th28; then A7: (f * f) . c <= f . c by FUZZY_1:def_2; f . c <= g . c by A2, XXREAL_0:def_9; then (f . c) * (f . c) <= (g . c) * (f . c) by A6, XREAL_1:64; then (f . c) * (f . c) <= (g . c) * (h . c) by A5, XXREAL_0:2; then min (((f * f) . c),((f . c) * (f . c))) <= min ((f . c),((g . c) * (h . c))) by A7, XXREAL_0:18; then min (((f . c) * (f . c)),((f . c) * (f . c))) <= min ((f . c),((g . c) * (h . c))) by Def2; then (f . c) * (f . c) <= min ((f . c),((g * h) . c)) by Def2; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c by A2, A3, FUZZY_1:5; ::_thesis: verum end; supposeA8: min ((f . c),(h . c)) = h . c ; ::_thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c A9: 1 >= h . c by Th1; A10: h . c >= 0 by Th1; f . c <= g . c by A2, XXREAL_0:def_9; then A11: (f . c) * (h . c) <= (g . c) * (h . c) by A10, XREAL_1:64; f . c >= 0 by Th1; then (f . c) * (h . c) <= (f . c) * 1 by A9, XREAL_1:64; then (f . c) * (h . c) <= min ((f . c),((g . c) * (h . c))) by A11, XXREAL_0:20; then (f . c) * (h . c) <= min ((f . c),((g * h) . c)) by Def2; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c by A2, A8, FUZZY_1:5; ::_thesis: verum end; end; end; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c ; ::_thesis: verum end; supposeA12: min ((f . c),(g . c)) = g . c ; ::_thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c proof percases ( min ((f . c),(h . c)) = f . c or min ((f . c),(h . c)) = h . c ) by XXREAL_0:15; supposeA13: min ((f . c),(h . c)) = f . c ; ::_thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c A14: g . c >= 0 by Th1; f . c <= h . c by A13, XXREAL_0:def_9; then A15: (f . c) * (g . c) <= (h . c) * (g . c) by A14, XREAL_1:64; A16: 1 >= g . c by Th1; f . c >= 0 by Th1; then (g . c) * (f . c) <= (f . c) * 1 by A16, XREAL_1:64; then (f . c) * (g . c) <= min ((f . c),((h . c) * (g . c))) by A15, XXREAL_0:20; then (f . c) * (g . c) <= min ((f . c),((g * h) . c)) by Def2; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c by A12, A13, FUZZY_1:5; ::_thesis: verum end; supposeA17: min ((f . c),(h . c)) = h . c ; ::_thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c A18: g . c <= f . c by A12, XXREAL_0:def_9; f . c >= 0 by Th1; then A19: (g . c) * (f . c) <= (f . c) * (f . c) by A18, XREAL_1:64; f c= by Th28; then (f * f) . c <= f . c by FUZZY_1:def_2; then A20: (f . c) * (f . c) <= f . c by Def2; A21: h . c <= f . c by A17, XXREAL_0:def_9; g . c >= 0 by Th1; then (h . c) * (g . c) <= (f . c) * (g . c) by A21, XREAL_1:64; then (h . c) * (g . c) <= (f . c) * (f . c) by A19, XXREAL_0:2; then (h . c) * (g . c) <= f . c by A20, XXREAL_0:2; then (h . c) * (g . c) <= min ((f . c),((h . c) * (g . c))) by XXREAL_0:20; then (g . c) * (h . c) <= min ((f . c),((g * h) . c)) by Def2; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c by A12, A17, FUZZY_1:5; ::_thesis: verum end; end; end; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c ; ::_thesis: verum end; end; end; hence (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . c ; ::_thesis: verum end; ((min (f,g)) * (min (f,h))) . c = ((min (f,g)) . c) * ((min (f,h)) . c) by Def2 .= (min ((f . c),(g . c))) * ((min (f,h)) . c) by FUZZY_1:5 .= (min ((f . c),(g . c))) * (min ((f . c),(h . c))) by FUZZY_1:5 ; hence ((min (f,g)) * (min (f,h))) . c <= (min (f,(g * h))) . c by A1; ::_thesis: verum end; theorem Th49: :: FUZZY_2:49 for C being non empty set for c being Element of C for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c))) proof let C be non empty set ; ::_thesis: for c being Element of C for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c))) let c be Element of C; ::_thesis: for f, g being Membership_Func of C holds (f ++ g) . c = 1 - ((1 - (f . c)) * (1 - (g . c))) let g, h be Membership_Func of C; ::_thesis: (g ++ h) . c = 1 - ((1 - (g . c)) * (1 - (h . c))) (g ++ h) . c = (1_minus ((1_minus g) * (1_minus h))) . c by Th36 .= 1 - (((1_minus g) * (1_minus h)) . c) by FUZZY_1:def_5 .= 1 - (((1_minus g) . c) * ((1_minus h) . c)) by Def2 .= 1 - ((1 - (g . c)) * ((1_minus h) . c)) by FUZZY_1:def_5 ; hence (g ++ h) . c = 1 - ((1 - (g . c)) * (1 - (h . c))) by FUZZY_1:def_5; ::_thesis: verum end; theorem :: FUZZY_2:50 for C being non empty set for f, g, h being Membership_Func of C holds (max (f,g)) ++ (max (f,h)) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (max (f,g)) ++ (max (f,h)) c= let f, g, h be Membership_Func of C; ::_thesis: (max (f,g)) ++ (max (f,h)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (max (f,(g ++ h))) . c <= ((max (f,g)) ++ (max (f,h))) . c A1: ((max (f,g)) ++ (max (f,h))) . c = (((max (f,g)) . c) + ((max (f,h)) . c)) - (((max (f,g)) . c) * ((max (f,h)) . c)) by Def3 .= ((max ((f . c),(g . c))) + ((max (f,h)) . c)) - (((max (f,g)) . c) * ((max (f,h)) . c)) by FUZZY_1:5 .= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - (((max (f,g)) . c) * ((max (f,h)) . c)) by FUZZY_1:5 .= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * ((max (f,h)) . c)) by FUZZY_1:5 .= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) by FUZZY_1:5 ; A2: max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) proof percases ( ( max ((f . c),(g . c)) = f . c & max ((f . c),(h . c)) = f . c ) or ( max ((f . c),(g . c)) = f . c & max ((f . c),(h . c)) = h . c ) or ( max ((f . c),(g . c)) = g . c & max ((f . c),(h . c)) = f . c ) or ( max ((f . c),(g . c)) = g . c & max ((f . c),(h . c)) = h . c ) ) by XXREAL_0:16; supposeA3: ( max ((f . c),(g . c)) = f . c & max ((f . c),(h . c)) = f . c ) ; ::_thesis: max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) (1_minus g) . c >= 0 by Th1; then A4: 1 - (g . c) >= 0 by FUZZY_1:def_5; h . c <= f . c by A3, XXREAL_0:def_10; then 1 - (h . c) >= 1 - (f . c) by XREAL_1:10; then A5: (1 - (g . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (h . c)) by A4, XREAL_1:64; (1_minus f) . c >= 0 by Th1; then A6: 1 - (f . c) >= 0 by FUZZY_1:def_5; f ++ f c= by Th28; then (f ++ f) . c >= f . c by FUZZY_1:def_2; then A7: ((f . c) + (f . c)) - ((f . c) * (f . c)) >= f . c by Def3; g . c <= f . c by A3, XXREAL_0:def_10; then 1 - (g . c) >= 1 - (f . c) by XREAL_1:10; then (1 - (f . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (f . c)) by A6, XREAL_1:64; then (1 - (f . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (h . c)) by A5, XXREAL_0:2; then 1 - ((1 - (f . c)) * (1 - (f . c))) >= 1 - ((1 - (g . c)) * (1 - (h . c))) by XREAL_1:10; hence max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) by A3, A7, XXREAL_0:28; ::_thesis: verum end; supposeA8: ( max ((f . c),(g . c)) = f . c & max ((f . c),(h . c)) = h . c ) ; ::_thesis: max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) (1_minus f) . c >= 0 by Th1; then A9: 1 - (f . c) >= 0 by FUZZY_1:def_5; h . c >= 0 by Th1; then 0 * (h . c) <= (h . c) * (1 - (f . c)) by A9, XREAL_1:64; then A10: 0 + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; (1_minus h) . c >= 0 by Th1; then A11: 1 - (h . c) >= 0 by FUZZY_1:def_5; g . c <= f . c by A8, XXREAL_0:def_10; then 1 - (f . c) <= 1 - (g . c) by XREAL_1:10; then (1 - (f . c)) * (1 - (h . c)) <= (1 - (g . c)) * (1 - (h . c)) by A11, XREAL_1:64; then 1 - ((1 - (f . c)) * (1 - (h . c))) >= 1 - ((1 - (g . c)) * (1 - (h . c))) by XREAL_1:10; hence max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) by A8, A10, XXREAL_0:28; ::_thesis: verum end; supposeA12: ( max ((f . c),(g . c)) = g . c & max ((f . c),(h . c)) = f . c ) ; ::_thesis: max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) (1_minus f) . c >= 0 by Th1; then A13: 1 - (f . c) >= 0 by FUZZY_1:def_5; g . c >= 0 by Th1; then 0 * (g . c) <= (g . c) * (1 - (f . c)) by A13, XREAL_1:64; then A14: 0 + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; (1_minus g) . c >= 0 by Th1; then A15: 1 - (g . c) >= 0 by FUZZY_1:def_5; h . c <= f . c by A12, XXREAL_0:def_10; then 1 - (f . c) <= 1 - (h . c) by XREAL_1:10; then (1 - (f . c)) * (1 - (g . c)) <= (1 - (h . c)) * (1 - (g . c)) by A15, XREAL_1:64; then 1 - ((1 - (f . c)) * (1 - (g . c))) >= 1 - ((1 - (h . c)) * (1 - (g . c))) by XREAL_1:10; hence max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) by A12, A14, XXREAL_0:28; ::_thesis: verum end; supposeA16: ( max ((f . c),(g . c)) = g . c & max ((f . c),(h . c)) = h . c ) ; ::_thesis: max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) (1_minus g) . c >= 0 by Th1; then A17: 1 - (g . c) >= 0 by FUZZY_1:def_5; h . c >= f . c by A16, XXREAL_0:def_10; then 1 - (h . c) <= 1 - (f . c) by XREAL_1:10; then A18: (1 - (g . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (h . c)) by A17, XREAL_1:64; (1_minus f) . c >= 0 by Th1; then A19: 1 - (f . c) >= 0 by FUZZY_1:def_5; g . c >= f . c by A16, XXREAL_0:def_10; then 1 - (g . c) <= 1 - (f . c) by XREAL_1:10; then (1 - (f . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (f . c)) by A19, XREAL_1:64; then (1 - (f . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (h . c)) by A18, XXREAL_0:2; then 1 - ((1 - (f . c)) * (1 - (f . c))) <= 1 - ((1 - (g . c)) * (1 - (h . c))) by XREAL_1:10; then A20: (f ++ f) . c <= 1 - ((1 - (g . c)) * (1 - (h . c))) by Th49; f ++ f c= by Th28; then (f ++ f) . c >= f . c by FUZZY_1:def_2; then f . c <= 1 - ((1 - (g . c)) * (1 - (h . c))) by A20, XXREAL_0:2; hence max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c)))) by A16, XXREAL_0:28; ::_thesis: verum end; end; end; (max (f,(g ++ h))) . c = max ((f . c),((g ++ h) . c)) by FUZZY_1:5 .= max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) by Th49 ; hence (max (f,(g ++ h))) . c <= ((max (f,g)) ++ (max (f,h))) . c by A1, A2; ::_thesis: verum end; theorem :: FUZZY_2:51 for C being non empty set for f, g, h being Membership_Func of C holds (min (f,g)) ++ (min (f,h)) c= proof let C be non empty set ; ::_thesis: for f, g, h being Membership_Func of C holds (min (f,g)) ++ (min (f,h)) c= let f, g, h be Membership_Func of C; ::_thesis: (min (f,g)) ++ (min (f,h)) c= let c be Element of C; :: according to FUZZY_1:def_2 ::_thesis: (min (f,(g ++ h))) . c <= ((min (f,g)) ++ (min (f,h))) . c A1: ((min (f,g)) ++ (min (f,h))) . c = (((min (f,g)) . c) + ((min (f,h)) . c)) - (((min (f,g)) . c) * ((min (f,h)) . c)) by Def3 .= ((min ((f . c),(g . c))) + ((min (f,h)) . c)) - (((min (f,g)) . c) * ((min (f,h)) . c)) by FUZZY_1:5 .= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - (((min (f,g)) . c) * ((min (f,h)) . c)) by FUZZY_1:5 .= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * ((min (f,h)) . c)) by FUZZY_1:5 .= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by FUZZY_1:5 ; A2: min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) proof now__::_thesis:_min_((f_._c),(1_-_((1_-_(g_._c))_*_(1_-_(h_._c)))))_<=_((min_((f_._c),(g_._c)))_+_(min_((f_._c),(h_._c))))_-_((min_((f_._c),(g_._c)))_*_(min_((f_._c),(h_._c)))) percases ( ( min ((f . c),(g . c)) = f . c & min ((f . c),(h . c)) = f . c ) or ( min ((f . c),(g . c)) = f . c & min ((f . c),(h . c)) = h . c ) or ( min ((f . c),(g . c)) = g . c & min ((f . c),(h . c)) = f . c ) or ( min ((f . c),(g . c)) = g . c & min ((f . c),(h . c)) = h . c ) ) by XXREAL_0:15; supposeA3: ( min ((f . c),(g . c)) = f . c & min ((f . c),(h . c)) = f . c ) ; ::_thesis: min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) f ++ f c= by Th28; then A4: (f ++ f) . c >= f . c by FUZZY_1:def_2; min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= f . c by XXREAL_0:17; then min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= (f ++ f) . c by A4, XXREAL_0:2; hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by A3, Def3; ::_thesis: verum end; supposeA5: ( min ((f . c),(g . c)) = f . c & min ((f . c),(h . c)) = h . c ) ; ::_thesis: min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) (1_minus f) . c >= 0 by Th1; then A6: 1 - (f . c) >= 0 by FUZZY_1:def_5; h . c >= 0 by Th1; then 0 * (h . c) <= (h . c) * (1 - (f . c)) by A6, XREAL_1:64; then A7: 0 + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= f . c by XXREAL_0:17; hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by A5, A7, XXREAL_0:2; ::_thesis: verum end; supposeA8: ( min ((f . c),(g . c)) = g . c & min ((f . c),(h . c)) = f . c ) ; ::_thesis: min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) (1_minus f) . c >= 0 by Th1; then A9: 1 - (f . c) >= 0 by FUZZY_1:def_5; g . c >= 0 by Th1; then 0 * (g . c) <= (g . c) * (1 - (f . c)) by A9, XREAL_1:64; then A10: 0 + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:6; min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= f . c by XXREAL_0:17; hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by A8, A10, XXREAL_0:2; ::_thesis: verum end; suppose ( min ((f . c),(g . c)) = g . c & min ((f . c),(h . c)) = h . c ) ; ::_thesis: min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) by XXREAL_0:17; ::_thesis: verum end; end; end; hence min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((min ((f . c),(g . c))) + (min ((f . c),(h . c)))) - ((min ((f . c),(g . c))) * (min ((f . c),(h . c)))) ; ::_thesis: verum end; (min (f,(g ++ h))) . c = min ((f . c),((g ++ h) . c)) by FUZZY_1:5 .= min ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) by Th49 ; hence (min (f,(g ++ h))) . c <= ((min (f,g)) ++ (min (f,h))) . c by A1, A2; ::_thesis: verum end; begin registration let C be non empty set ; clusterV20([.0,1.]) V21() quasi_total -> for Element of bool [:C,REAL:]; coherence for b1 being Membership_Func of C holds b1 is quasi_total ; end; definition let C1, C2 be non empty set ; mode RMembership_Func of C1,C2 is Membership_Func of [:C1,C2:]; end; definition let C1, C2 be non empty set ; func Zmf (C1,C2) -> RMembership_Func of C1,C2 equals :: FUZZY_2:def 4 chi ({},[:C1,C2:]); correctness coherence chi ({},[:C1,C2:]) is RMembership_Func of C1,C2; by FUZZY_1:12; func Umf (C1,C2) -> RMembership_Func of C1,C2 equals :: FUZZY_2:def 5 chi ([:C1,C2:],[:C1,C2:]); correctness coherence chi ([:C1,C2:],[:C1,C2:]) is RMembership_Func of C1,C2; by FUZZY_1:1; end; :: deftheorem defines Zmf FUZZY_2:def_4_:_ for C1, C2 being non empty set holds Zmf (C1,C2) = chi ({},[:C1,C2:]); :: deftheorem defines Umf FUZZY_2:def_5_:_ for C1, C2 being non empty set holds Umf (C1,C2) = chi ([:C1,C2:],[:C1,C2:]); theorem :: FUZZY_2:52 for C1, C2 being non empty set for x being Element of [:C1,C2:] for h being RMembership_Func of C1,C2 holds ( (Zmf (C1,C2)) . x <= h . x & h . x <= (Umf (C1,C2)) . x ) proof let C1, C2 be non empty set ; ::_thesis: for x being Element of [:C1,C2:] for h being RMembership_Func of C1,C2 holds ( (Zmf (C1,C2)) . x <= h . x & h . x <= (Umf (C1,C2)) . x ) A1: Umf (C1,C2) = UMF [:C1,C2:] ; Zmf (C1,C2) = EMF [:C1,C2:] ; hence for x being Element of [:C1,C2:] for h being RMembership_Func of C1,C2 holds ( (Zmf (C1,C2)) . x <= h . x & h . x <= (Umf (C1,C2)) . x ) by A1, FUZZY_1:16; ::_thesis: verum end; theorem :: FUZZY_2:53 for C1, C2 being non empty set for f being RMembership_Func of C1,C2 holds ( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) ) proof let C1, C2 be non empty set ; ::_thesis: for f being RMembership_Func of C1,C2 holds ( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) ) let f be RMembership_Func of C1,C2; ::_thesis: ( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) ) A1: Umf (C1,C2) = UMF [:C1,C2:] ; Zmf (C1,C2) = EMF [:C1,C2:] ; hence ( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) ) by A1, FUZZY_1:18; ::_thesis: verum end; theorem :: FUZZY_2:54 for C1, C2 being non empty set holds ( 1_minus (Zmf (C1,C2)) = Umf (C1,C2) & 1_minus (Umf (C1,C2)) = Zmf (C1,C2) ) proof let C1, C2 be non empty set ; ::_thesis: ( 1_minus (Zmf (C1,C2)) = Umf (C1,C2) & 1_minus (Umf (C1,C2)) = Zmf (C1,C2) ) A1: Umf (C1,C2) = UMF [:C1,C2:] ; Zmf (C1,C2) = EMF [:C1,C2:] ; hence ( 1_minus (Zmf (C1,C2)) = Umf (C1,C2) & 1_minus (Umf (C1,C2)) = Zmf (C1,C2) ) by A1, FUZZY_1:40; ::_thesis: verum end; theorem :: FUZZY_2:55 for C1, C2 being non empty set for f, g being RMembership_Func of C1,C2 st f \ g = Zmf (C1,C2) holds g c= proof let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 st f \ g = Zmf (C1,C2) holds g c= let f, g be RMembership_Func of C1,C2; ::_thesis: ( f \ g = Zmf (C1,C2) implies g c= ) Zmf (C1,C2) = EMF [:C1,C2:] ; hence ( f \ g = Zmf (C1,C2) implies g c= ) by Th26; ::_thesis: verum end; theorem :: FUZZY_2:56 for C1, C2 being non empty set for f, g being RMembership_Func of C1,C2 st min (f,g) = Zmf (C1,C2) holds f \ g = f proof let C1, C2 be non empty set ; ::_thesis: for f, g being RMembership_Func of C1,C2 st min (f,g) = Zmf (C1,C2) holds f \ g = f let f, g be RMembership_Func of C1,C2; ::_thesis: ( min (f,g) = Zmf (C1,C2) implies f \ g = f ) Zmf (C1,C2) = EMF [:C1,C2:] ; hence ( min (f,g) = Zmf (C1,C2) implies f \ g = f ) by Th27; ::_thesis: verum end;