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

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

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

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

end;

((min (f,g)) * (min (f,h))) . c =
((min (f,g)) . c) * ((min (f,h)) . c)
by Def2
now :: thesis: (min ((f . c),(g . c))) * (min ((f . c),(h . c))) <= (min (f,(g * h))) . cend;

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

end;

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

end;proof
end;

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

end;

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

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

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

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

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

end;proof
end;

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

end;

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

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

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

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

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