let C be non empty set ; for f, h, g being Membership_Func of C holds f ++ (g * h) c=
let f, h, g be Membership_Func of C; f ++ (g * h) c=
let c be Element of C; FUZZY_1:def 2 ((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
;
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; verum