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 3 :: thesis: ((max f,g) * (max f,h)) . c <= (max f,(g * h)) . c
A1: ((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:6
.= (max (f . c),(g . c)) * (max (f . c),(h . c)) by FUZZY_1:6 ;
(max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c

proof

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

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

proof

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

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 . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c

proof

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

hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c ; :: thesis: verum

end;

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

(max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c

proof

( f . c >= 0 & 1 >= h . c ) by Th1;
then A6: (f . c) * (h . c) <= (f . c) * 1 by XREAL_1:66;
f . c <= max (f . c),((g * h) . c) by XXREAL_0:25;
then f . c <= (max f,(g * h)) . c by FUZZY_1:6;
hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c by A2, A5, A6, XXREAL_0:2; :: thesis: verum

end;

hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c ; :: thesis: verum

end;

end;

end;

hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c ; :: thesis: verum

end;

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

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

suppose A8: 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 . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c

proof

( f . c >= 0 & 1 >= g . c ) by Th1;
then A9: (f . c) * (g . c) <= (f . c) * 1 by XREAL_1:66;
f . c <= max (f . c),((g * h) . c) by XXREAL_0:25;
then f . c <= (max f,(g * h)) . c by FUZZY_1:6;
hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c by A7, A8, A9, XXREAL_0:2; :: thesis: verum

end;

hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c ; :: thesis: verum

end;

suppose A10: 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 . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c

proof

(max f,(g * h)) . c = max (f . c),((g * h) . c) by FUZZY_1:6;
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 A7, A10, Def2; :: thesis: verum

end;

hence (max (f . c),(g . c)) * (max (f . c),(h . c)) <= (max f,(g * h)) . c ; :: 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;

hence ((max f,g) * (max f,h)) . c <= (max f,(g * h)) . c by A1; :: thesis: verum