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

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

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

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

((max (f,g)) * (max (f,h))) . c =
((max (f,g)) . c) * ((max (f,h)) . c)
by Def2
per cases
( max ((f . c),(g . c)) = f . c or max ((f . c),(g . c)) = g . c )
by XXREAL_0:16;

end;

suppose A2:
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

end;proof
end;

hence
(max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c
; :: thesis: verumper cases
( max ((f . c),(h . c)) = f . c or max ((f . c),(h . c)) = h . c )
by XXREAL_0:16;

end;

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

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;then A4: (max (f,(g * h))) . c >= f . c by XXREAL_0:25;

f c= by Th28;

then (f * f) . c <= f . c ;

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

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

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

end;proof
end;

hence
(max ((f . c),(g . c))) * (max ((f . c),(h . c))) <= (max (f,(g * h))) . c
; :: thesis: verumper cases
( max ((f . c),(h . c)) = f . c or max ((f . c),(h . c)) = h . c )
by XXREAL_0:16;

end;

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

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

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