let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds f ++ (min (g,h)) = min ((f ++ g),(f ++ h))
let f, h, g be Membership_Func of C; :: thesis: f ++ (min (g,h)) = min ((f ++ g),(f ++ h))
A1: C = dom (min ((f ++ g),(f ++ h))) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds
(f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c

proof

let c be Element of C; :: thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c )
A3: (f ++ (min (g,h))) . c = ((f . c) + ((min (g,h)) . c)) - ((f . c) * ((min (g,h)) . c)) by Def3
.= ((f . c) + (min ((g . c),(h . c)))) - ((f . c) * ((min (g,h)) . c)) by FUZZY_1:5 ;

now :: thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c )

per cases ( min ((g . c),(h . c)) = g . c or min ((g . c),(h . c)) = h . c ) by XXREAL_0:15;

suppose A4: min ((g . c),(h . c)) = g . c ; :: thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c )

A5: (1_minus f) . c >= 0 by Th1;
g . c <= h . c by A4, XXREAL_0:def 9;
then (g . c) * ((1_minus f) . c) <= (h . c) * ((1_minus f) . c) by A5, XREAL_1:64;
then (g . c) * (1 - (f . c)) <= (h . c) * ((1_minus f) . c) by FUZZY_1:def 5;
then (g . c) * (1 - (f . c)) <= (h . c) * (1 - (f . c)) by FUZZY_1:def 5;
then (((g . c) * 1) - ((g . c) * (f . c))) + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c) by XREAL_1:6;
then A6: ((f . c) + (g . c)) - ((f . c) * (g . c)) = min ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by XXREAL_0:def 9
.= min (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by Def3
.= min (((f ++ g) . c),((f ++ h) . c)) by Def3 ;
(f ++ (min (g,h))) . c = ((f . c) + (g . c)) - ((f . c) * (g . c)) by A3, A4, FUZZY_1:5;
hence ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) by A6, FUZZY_1:5; :: thesis: verum

end;

suppose A7: min ((g . c),(h . c)) = h . c ; :: thesis: ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c )

A8: (1_minus f) . c >= 0 by Th1;
h . c <= g . c by A7, XXREAL_0:def 9;
then (h . c) * ((1_minus f) . c) <= (g . c) * ((1_minus f) . c) by A8, XREAL_1:64;
then (h . c) * (1 - (f . c)) <= (g . c) * ((1_minus f) . c) by FUZZY_1:def 5;
then (h . c) * (1 - (f . c)) <= (g . c) * (1 - (f . c)) by FUZZY_1:def 5;
then (((h . c) * 1) - ((h . c) * (f . c))) + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c) by XREAL_1:6;
then A9: ((f . c) + (h . c)) - ((f . c) * (h . c)) = min ((((f . c) + (g . c)) - ((f . c) * (g . c))),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by XXREAL_0:def 9
.= min (((f ++ g) . c),(((f . c) + (h . c)) - ((f . c) * (h . c)))) by Def3
.= min (((f ++ g) . c),((f ++ h) . c)) by Def3 ;
(f ++ (min (g,h))) . c = ((f . c) + (h . c)) - ((f . c) * (h . c)) by A3, A7, FUZZY_1:5;
hence ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) by A9, FUZZY_1:5; :: thesis: verum

end;

end;

end;

hence ( c in C implies (f ++ (min (g,h))) . c = (min ((f ++ g),(f ++ h))) . c ) ; :: thesis: verum

end;

C = dom (f ++ (min (g,h))) by FUNCT_2:def 1;
hence f ++ (min (g,h)) = min ((f ++ g),(f ++ h)) by A1, A2, PARTFUN1:5; :: thesis: verum