let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds f * (max (g,h)) = max ((f * g),(f * h))

let f, h, g be Membership_Func of C; :: thesis: f * (max (g,h)) = max ((f * g),(f * h))

A1: C = dom (max ((f * g),(f * h))) by FUNCT_2:def 1;

A2: for c being Element of C st c in C holds

(f * (max (g,h))) . c = (max ((f * g),(f * h))) . c

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

let f, h, g be Membership_Func of C; :: thesis: f * (max (g,h)) = max ((f * g),(f * h))

A1: C = dom (max ((f * g),(f * h))) by FUNCT_2:def 1;

A2: for c being Element of C st c in C holds

(f * (max (g,h))) . c = (max ((f * g),(f * h))) . c

proof

C = dom (f * (max (g,h)))
by FUNCT_2:def 1;
let c be Element of C; :: thesis: ( c in C implies (f * (max (g,h))) . c = (max ((f * g),(f * h))) . c )

(f * (max (g,h))) . c = (f . c) * ((max (g,h)) . c) by Def2

.= (f . c) * (max ((g . c),(h . c))) by FUZZY_1:5

.= max (((f . c) * (g . c)),((f . c) * (h . c))) by Lm2, Th1

.= 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:5; :: thesis: verum

end;(f * (max (g,h))) . c = (f . c) * ((max (g,h)) . c) by Def2

.= (f . c) * (max ((g . c),(h . c))) by FUZZY_1:5

.= max (((f . c) * (g . c)),((f . c) * (h . c))) by Lm2, Th1

.= 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:5; :: thesis: verum

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