let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds

( f c= & f ++ (f * g) c= )

let f, g be Membership_Func of C; :: thesis: ( f c= & f ++ (f * g) c= )

thus f c= :: thesis: f ++ (f * g) c=

A2: (1_minus f) . c >= 0 by Th1;

(f * g) . c >= 0 by Th1;

then 0 * ((f * g) . c) <= ((1_minus f) . c) * ((f * g) . c) by A2, XREAL_1:64;

then 0 <= (1 - (f . c)) * ((f * g) . c) by FUZZY_1:def 5;

then 0 + (f . c) <= (((f * g) . c) - ((f . c) * ((f * g) . c))) + (f . c) by XREAL_1:6;

then f . c <= ((f . c) + ((f * g) . c)) - ((f . c) * ((f * g) . c)) ;

hence f . c <= (f ++ (f * g)) . c by Def3; :: thesis: verum

( f c= & f ++ (f * g) c= )

let f, g be Membership_Func of C; :: thesis: ( f c= & f ++ (f * g) c= )

thus f c= :: thesis: f ++ (f * g) c=

proof

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: f . c <= (f ++ (f * g)) . c
let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (f * (f ++ g)) . c <= f . c

A1: (f ++ g) . c <= 1 by Th1;

0 <= f . c by Th1;

then ((f ++ g) . c) * (f . c) <= 1 * (f . c) by A1, XREAL_1:64;

hence (f * (f ++ g)) . c <= f . c by Def2; :: thesis: verum

end;A1: (f ++ g) . c <= 1 by Th1;

0 <= f . c by Th1;

then ((f ++ g) . c) * (f . c) <= 1 * (f . c) by A1, XREAL_1:64;

hence (f * (f ++ g)) . c <= f . c by Def2; :: thesis: verum

A2: (1_minus f) . c >= 0 by Th1;

(f * g) . c >= 0 by Th1;

then 0 * ((f * g) . c) <= ((1_minus f) . c) * ((f * g) . c) by A2, XREAL_1:64;

then 0 <= (1 - (f . c)) * ((f * g) . c) by FUZZY_1:def 5;

then 0 + (f . c) <= (((f * g) . c) - ((f . c) * ((f * g) . c))) + (f . c) by XREAL_1:6;

then f . c <= ((f . c) + ((f * g) . c)) - ((f . c) * ((f * g) . c)) ;

hence f . c <= (f ++ (f * g)) . c by Def3; :: thesis: verum