let C1, C2, C3 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds (max f,g) (#) h = max (f (#) h),(g (#) h)
let f, g be RMembership_Func of C1,C2; :: thesis: for h being RMembership_Func of C2,C3 holds (max f,g) (#) h = max (f (#) h),(g (#) h)
let h be RMembership_Func of C2,C3; :: thesis: (max f,g) (#) h = max (f (#) h),(g (#) h)
A1: ( dom ((max f,g) (#) h) = [:C1,C3:] & dom (f (#) h) = [:C1,C3:] & dom (max (f (#) h),(g (#) h)) = [:C1,C3:] & dom (g (#) h) = [:C1,C3:] ) by FUNCT_2:def 1;
for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
((max f,g) (#) h) . c = (max (f (#) h),(g (#) h)) . c

proof

let c be Element of [:C1,C3:]; :: thesis: ( c in [:C1,C3:] implies ((max f,g) (#) h) . c = (max (f (#) h),(g (#) h)) . c )
consider x, z being set such that
A2: ( x in C1 & z in C3 & c = [x,z] ) by ZFMISC_1:def 2;
((max f,g) (#) h) . c = ((max f,g) (#) h) . x,z by A2
.= sup (rng (min (max f,g),h,x,z)) by A2, Def3
.= max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z))) by A2, Lm2
.= max ((f (#) h) . x,z),(sup (rng (min g,h,x,z))) by A2, Def3
.= max ((f (#) h) . x,z),((g (#) h) . x,z) by A2, Def3
.= (max (f (#) h),(g (#) h)) . c by A2, FUZZY_1:def 5 ;
hence ( c in [:C1,C3:] implies ((max f,g) (#) h) . c = (max (f (#) h),(g (#) h)) . c ) ; :: thesis: verum

end;

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