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

proof

let c be Element of [:C1,C3:]; :: thesis: ( c in [:C1,C3:] implies (f (#) (max (g,h))) . c = (max ((f (#) g),(f (#) h))) . c )
consider x, z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
reconsider z = z, x = x as set by TARSKI:1;
(f (#) (max (g,h))) . c = (f (#) (max (g,h))) . (x,z) by A5
.= upper_bound (rng (min (f,(max (g,h)),x,z))) by A5, Def3
.= max ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A3, A4, Lm1
.= max (((f (#) g) . (x,z)),(upper_bound (rng (min (f,h,x,z))))) by A5, Def3
.= max (((f (#) g) . (x,z)),((f (#) h) . (x,z))) by A5, Def3
.= (max ((f (#) g),(f (#) h))) . c by A5, FUZZY_1:def 4 ;
hence ( c in [:C1,C3:] implies (f (#) (max (g,h))) . c = (max ((f (#) g),(f (#) h))) . c ) ; :: thesis: verum

end;

dom (f (#) (max (g,h))) = [:C1,C3:] by FUNCT_2:def 1;
hence f (#) (max (g,h)) = max ((f (#) g),(f (#) h)) by A1, A2, PARTFUN1:5; :: thesis: verum