let C1, C2, C3 be non empty set ; for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3
for x, z being set st 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] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
let f, g be RMembership_Func of C1,C2; for h, k being RMembership_Func of C2,C3
for x, z being set st 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] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
let h, k be RMembership_Func of C2,C3; for x, z being set st 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] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
let x, z be set ; ( 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] ) ) implies (f (#) h) . [x,z] <= (g (#) k) . [x,z] )
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] )
; (f (#) h) . [x,z] <= (g (#) k) . [x,z]
A4:
[x,z] in [:C1,C3:]
by A1, A2, ZFMISC_1:87;
then A5:
(g (#) k) . (x,z) = upper_bound (rng (min (g,k,x,z)))
by Def3;
rng (min (f,h,x,z)) is real-bounded
by Th1;
then A6:
rng (min (f,h,x,z)) is bounded_above
by XXREAL_2:def 11;
A7:
for s being Real st s > 0 holds
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z)))
proof
let s be
Real;
( s > 0 implies (upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z))) )
assume
s > 0
;
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z)))
then consider r being
Real such that A8:
r in rng (min (f,h,x,z))
and A9:
(upper_bound (rng (min (f,h,x,z)))) - s < r
by A6, SEQ_4:def 1;
consider y being
object 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 3;
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]))
<= upper_bound (rng (min (g,k,x,z)))
by A14, Th1;
then
(min (f,h,x,z)) . y <= upper_bound (rng (min (g,k,x,z)))
by A13, XXREAL_0:2;
hence
(upper_bound (rng (min (f,h,x,z)))) - s <= upper_bound (rng (min (g,k,x,z)))
by A9, A11, XXREAL_0:2;
verum
end;
(f (#) h) . (x,z) = upper_bound (rng (min (f,h,x,z)))
by A4, Def3;
hence
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
by A5, A7, XREAL_1:57; verum