let C1, C2, C3 be non empty set ; :: thesis:
let f, g be RMembership_Func of C1,C2; :: thesis:
let h, k be RMembership_Func of C2,C3; :: thesis:
let x, z be set ; :: thesis:
assume A1: ( x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) ) ; :: thesis:
then [x,z] in [:C1,C3:] by ZFMISC_1:106;
then A2: ( (f (#) h) . x,z = sup (rng (min f,h,x,z)) & (g (#) k) . x,z = sup (rng (min g,k,x,z)) ) by Def3;
sup (rng (min f,h,x,z)) <= sup (rng (min g,k,x,z))

rng (min f,h,x,z) is bounded by Th1;
then A3: rng (min f,h,x,z) is bounded_above by XXREAL_2:def 11;
for s being real number st s > 0 holds
(sup (rng (min f,h,x,z))) - s <= sup (rng (min g,k,x,z))

let s be real number ; :: thesis:
assume s > 0 ; :: thesis:
then consider r being real number such that
A4: ( r in rng (min f,h,x,z) & (sup (rng (min f,h,x,z))) - s < r ) by A3, SEQ_4:def 4;
consider y being set such that
A5: ( y in dom (min f,h,x,z) & r = (min f,h,x,z) . y ) by A4, FUNCT_1:def 5;
y in C2 by A5;
then A6: y in dom (min g,k,x,z) by FUNCT_2:def 1;
(min f,h,x,z) . y <= sup (rng (min g,k,x,z))

( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) by A1, A5;
then min (f . [x,y]),(h . [y,z]) <= min (g . [x,y]),(k . [y,z]) by XXREAL_0:18;
then A7: (min f,h,x,z) . y <= min (g . [x,y]),(k . [y,z]) by A1, A5, Def2;
min (g . [x,y]),(k . [y,z]) = (min g,k,x,z) . y by A1, A5, Def2;
then min (g . [x,y]),(k . [y,z]) <= sup (rng (min g,k,x,z)) by A6, Th1;
hence (min f,h,x,z) . y <= sup (rng (min g,k,x,z)) by A7, XXREAL_0:2; :: thesis:

end;

hence (sup (rng (min f,h,x,z))) - s <= sup (rng (min g,k,x,z)) by A4, A5, XXREAL_0:2; :: thesis:

end;

hence sup (rng (min f,h,x,z)) <= sup (rng (min g,k,x,z)) by XREAL_1:59; :: thesis:

end;

hence (f (#) h) . [x,z] <= (g (#) k) . [x,z] by A2; :: thesis: