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

let f, g be Membership_Func of C; :: thesis: f ++ g c=

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

A1: (max (f,g)) . c = max ((f . c),(g . c)) by FUZZY_1:5;

let f, g be Membership_Func of C; :: thesis: f ++ g c=

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

A1: (max (f,g)) . c = max ((f . c),(g . c)) by FUZZY_1:5;

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

end;

suppose A2:
(max (f,g)) . c = f . c
; :: thesis: (max (f,g)) . c <= (f ++ g) . c

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

g . c >= 0 by Th1;

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

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

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

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

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

end;g . c >= 0 by Th1;

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

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

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

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

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

suppose A4:
(max (f,g)) . c = g . c
; :: thesis: (max (f,g)) . c <= (f ++ g) . c

A5:
(1_minus g) . c >= 0
by Th1;

f . c >= 0 by Th1;

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

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

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

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

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

end;f . c >= 0 by Th1;

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

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

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

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

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