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 . c >= 0 by Th1;
(f * (max g,h)) . c = (f . c) * ((max g,h) . c) by Def2
.= (f . c) * (max (g . c),(h . c)) by FUZZY_1:6
.= max ((f . c) * (g . c)),((f . c) * (h . c)) by A2, Lm2
.= max ((f * g) . c),((f . c) * (h . c)) by Def2
.= max ((f * g) . c),((f * h) . c) by Def2 ;
hence ( c in C implies (f * (max g,h)) . c = (max (f * g),(f * h)) . c ) by FUZZY_1:6; :: thesis: verum

end;

hence f * (max g,h) = max (f * g),(f * h) by A1, PARTFUN1:34; :: thesis: verum