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