let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds (f * g) ++ (f * h) c=
let f, h, g be Membership_Func of C; :: thesis: (f * g) ++ (f * h) c=
let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (f * (g ++ h)) . c <= ((f * g) ++ (f * h)) . c
set x = f . c;
set y = g . c;
set z = h . c;
f c= by Th28;
then A1: (f * f) . c <= f . c ;
(g * h) . c >= 0 by Th1;
then ((f * f) . c) * ((g * h) . c) <= (f . c) * ((g * h) . c) by A1, XREAL_1:64;
then (((f * g) . c) + ((f * h) . c)) - (((f * f) . c) * ((g * h) . c)) >= (((f * g) . c) + ((f * h) . c)) - ((f . c) * ((g * h) . c)) by XREAL_1:10;
then (((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c) >= (((f * g) . c) + ((f * h) . c)) - ((f . c) * ((g * h) . c)) by Def2;
then (((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c) >= (((f . c) * (g . c)) + ((f * h) . c)) - ((f . c) * ((g * h) . c)) by Def2;
then (((f * g) . c) + ((f * h) . c)) - (((f * f) * (g * h)) . c) >= (((f . c) * (g . c)) + ((f . c) * (h . c))) - ((f . c) * ((g * h) . c)) by Def2;
then (((f * g) . c) + ((f * h) . c)) - ((f * (f * (g * h))) . c) >= (((f . c) * (g . c)) + ((f . c) * (h . c))) - ((f . c) * ((g * h) . c)) by Th29;
then (((f * g) . c) + ((f * h) . c)) - ((f * ((g * f) * h)) . c) >= (((g . c) + (h . c)) - ((g * h) . c)) * (f . c) by Th29;
then (((f * g) . c) + ((f * h) . c)) - (((f * g) * (f * h)) . c) >= (((g . c) + (h . c)) - ((g * h) . c)) * (f . c) by Th29;
then (((f * g) . c) + ((f * h) . c)) - (((f * g) * (f * h)) . c) >= (f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c))) by Def2;
then (((f * g) . c) + ((f * h) . c)) - (((f * g) . c) * ((f * h) . c)) >= (f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c))) by Def2;
then ((f * g) ++ (f * h)) . c >= (f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c))) by Def3;
then ((f * g) ++ (f * h)) . c >= (f . c) * ((g ++ h) . c) by Def3;
hence (f * (g ++ h)) . c <= ((f * g) ++ (f * h)) . c by Def2; :: thesis: verum