let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds (max (f,g)) ++ (max (f,h)) c=

let f, h, g 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))))

.= 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

let f, h, g 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
end;

(max (f,(g ++ h))) . c =
max ((f . c),((g ++ h) . c))
by FUZZY_1:5
per cases
( ( 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;

end;

suppose A3:
( 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 ;

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

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

suppose A8:
( 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;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

suppose A12:
( 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;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

suppose A16:
( 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 ;

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

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

.= 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