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 that
A1: x in C1 and
A2: z in C3 and
A3: for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ; :: thesis:
A4: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:106;
then A5: (g (#) k) . x,z = sup (rng (min g,k,x,z)) by Def3;
rng (min f,h,x,z) is bounded by Th1;
then A6: rng (min f,h,x,z) is bounded_above by XXREAL_2:def 11;
A7: 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
A8: r in rng (min f,h,x,z) and
A9: (sup (rng (min f,h,x,z))) - s < r by A6, SEQ_4:def 4;
consider y being set such that
A10: y in dom (min f,h,x,z) and
A11: r = (min f,h,x,z) . y by A8, FUNCT_1:def 5;
A12: h . [y,z] <= k . [y,z] by A3, A10;
f . [x,y] <= g . [x,y] by A3, A10;
then min (f . [x,y]),(h . [y,z]) <= min (g . [x,y]),(k . [y,z]) by A12, XXREAL_0:18;
then A13: (min f,h,x,z) . y <= min (g . [x,y]),(k . [y,z]) by A1, A2, A10, Def2;
y in C2 by A10;
then A14: y in dom (min g,k,x,z) by FUNCT_2:def 1;
min (g . [x,y]),(k . [y,z]) = (min g,k,x,z) . y by A1, A2, A10, Def2;
then min (g . [x,y]),(k . [y,z]) <= sup (rng (min g,k,x,z)) by A14, Th1;
then (min f,h,x,z) . y <= sup (rng (min g,k,x,z)) by A13, XXREAL_0:2;
hence (sup (rng (min f,h,x,z))) - s <= sup (rng (min g,k,x,z)) by A9, A11, XXREAL_0:2; :: thesis:

end;

(f (#) h) . x,z = sup (rng (min f,h,x,z)) by A4, Def3;
hence (f (#) h) . [x,z] <= (g (#) k) . [x,z] by A5, A7, XREAL_1:59; :: thesis: