let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds f ++ (max g,h) = max (f ++ g),(f ++ h)
let f, g, h be Membership_Func of C; :: thesis: f ++ (max g,h) = max (f ++ g),(f ++ h)
A1:
( C = dom (f ++ (max g,h)) & C = dom (max (f ++ g),(f ++ h)) )
by FUNCT_2:def 1;
for c being Element of C st c in C holds
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c
proof
let c be
Element of
C;
:: thesis: ( c in C implies (f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c )
A2:
(f ++ (max g,h)) . c =
((f . c) + ((max g,h) . c)) - ((f . c) * ((max g,h) . c))
by Def3
.=
((f . c) + (max (g . c),(h . c))) - ((f . c) * ((max g,h) . c))
by FUZZY_1:6
;
per cases
( max (g . c),(h . c) = g . c or max (g . c),(h . c) = h . c )
by XXREAL_0:16;
suppose A3:
max (g . c),
(h . c) = g . c
;
:: thesis: ( c in C implies (f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c )
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c
proof
(
g . c >= h . c &
(1_minus f) . c >= 0 )
by A3, Th1, XXREAL_0:def 10;
then
(g . c) * ((1_minus f) . c) >= (h . c) * ((1_minus f) . c)
by XREAL_1:66;
then
(g . c) * (1 - (f . c)) >= (h . c) * ((1_minus f) . c)
by FUZZY_1:def 6;
then
(g . c) * (1 - (f . c)) >= (h . c) * (1 - (f . c))
by FUZZY_1:def 6;
then A4:
(((g . c) * 1) - ((g . c) * (f . c))) + (f . c) >= ((h . c) * (1 - (f . c))) + (f . c)
by XREAL_1:8;
A5:
(f ++ (max g,h)) . c = ((f . c) + (g . c)) - ((f . c) * (g . c))
by A2, A3, FUZZY_1:6;
((f . c) + (g . c)) - ((f . c) * (g . c)) =
max (((f . c) + (g . c)) - ((f . c) * (g . c))),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by A4, XXREAL_0:def 10
.=
max ((f ++ g) . c),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by Def3
.=
max ((f ++ g) . c),
((f ++ h) . c)
by Def3
;
hence
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c
by A5, FUZZY_1:6;
:: thesis: verum
end; hence
(
c in C implies
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c )
;
:: thesis: verum end; suppose A6:
max (g . c),
(h . c) = h . c
;
:: thesis: ( c in C implies (f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c )
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c
proof
(
h . c >= g . c &
(1_minus f) . c >= 0 )
by A6, Th1, XXREAL_0:def 10;
then
(h . c) * ((1_minus f) . c) >= (g . c) * ((1_minus f) . c)
by XREAL_1:66;
then
(h . c) * (1 - (f . c)) >= (g . c) * ((1_minus f) . c)
by FUZZY_1:def 6;
then
(h . c) * (1 - (f . c)) >= (g . c) * (1 - (f . c))
by FUZZY_1:def 6;
then A7:
(((h . c) * 1) - ((h . c) * (f . c))) + (f . c) >= ((g . c) * (1 - (f . c))) + (f . c)
by XREAL_1:8;
A8:
(f ++ (max g,h)) . c = ((f . c) + (h . c)) - ((f . c) * (h . c))
by A2, A6, FUZZY_1:6;
((f . c) + (h . c)) - ((f . c) * (h . c)) =
max (((f . c) + (g . c)) - ((f . c) * (g . c))),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by A7, XXREAL_0:def 10
.=
max ((f ++ g) . c),
(((f . c) + (h . c)) - ((f . c) * (h . c)))
by Def3
.=
max ((f ++ g) . c),
((f ++ h) . c)
by Def3
;
hence
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c
by A8, FUZZY_1:6;
:: thesis: verum
end; hence
(
c in C implies
(f ++ (max g,h)) . c = (max (f ++ g),(f ++ h)) . c )
;
:: thesis: verum end;
end;
hence
f ++ (max g,h) = max (f ++ g),(f ++ h)
by A1, PARTFUN1:34; :: thesis: verum