let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
let f be RMembership_Func of C1,C2; :: thesis: for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
let g be RMembership_Func of C2,C3; :: thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
let x, z be set ; :: thesis: ( x in C1 & z in C3 implies upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z))) )
assume that
A1: x in C1 and
A2: z in C3 ; :: thesis: upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z)))
rng (min (f,g,x,z)) is real-bounded by Th1;
then A3: rng (min (f,g,x,z)) is bounded_above by XXREAL_2:def 11;
for s being Real st 0 < s holds
(upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x)))
proof
let s be Real; :: thesis: ( 0 < s implies (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x))) )
assume s > 0 ; :: thesis: (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x)))
then consider r being Real such that
A4: r in rng (min (f,g,x,z)) and
A5: (upper_bound (rng (min (f,g,x,z)))) - s < r by A3, SEQ_4:def 1;
consider y being object such that
A6: y in dom (min (f,g,x,z)) and
A7: r = (min (f,g,x,z)) . y by A4, FUNCT_1:def 3;
reconsider y = y as set by TARSKI:1;
A8: [z,y] in [:C3,C2:] by A2, A6, ZFMISC_1:87;
y in C2 by A6;
then y in dom (min ((converse g),(converse f),z,x)) by FUNCT_2:def 1;
then A9: (min ((converse g),(converse f),z,x)) . y <= upper_bound (rng (min ((converse g),(converse f),z,x))) by Th1;
A10: [y,x] in [:C2,C1:] by A1, A6, ZFMISC_1:87;
r = min ((f . (x,y)),(g . (y,z))) by A1, A2, A6, A7, Def2
.= min (((converse f) . (y,x)),(g . (y,z))) by A10, Def1
.= min (((converse f) . (y,x)),((converse g) . (z,y))) by A8, Def1
.= (min ((converse g),(converse f),z,x)) . y by A1, A2, A6, Def2 ;
hence (upper_bound (rng (min (f,g,x,z)))) - s <= upper_bound (rng (min ((converse g),(converse f),z,x))) by A5, A9, XXREAL_0:2; :: thesis: verum
end;
then A11: upper_bound (rng (min ((converse g),(converse f),z,x))) >= upper_bound (rng (min (f,g,x,z))) by XREAL_1:57;
rng (min ((converse g),(converse f),z,x)) is real-bounded by Th1;
then A12: rng (min ((converse g),(converse f),z,x)) is bounded_above by XXREAL_2:def 11;
for s being Real st 0 < s holds
(upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z)))
proof
let s be Real; :: thesis: ( 0 < s implies (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z))) )
assume s > 0 ; :: thesis: (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z)))
then consider r being Real such that
A13: r in rng (min ((converse g),(converse f),z,x)) and
A14: (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s < r by A12, SEQ_4:def 1;
consider y being object such that
A15: y in dom (min ((converse g),(converse f),z,x)) and
A16: r = (min ((converse g),(converse f),z,x)) . y by A13, FUNCT_1:def 3;
A17: [z,y] in [:C3,C2:] by A2, A15, ZFMISC_1:87;
y in C2 by A15;
then y in dom (min (f,g,x,z)) by FUNCT_2:def 1;
then A18: (min (f,g,x,z)) . y <= upper_bound (rng (min (f,g,x,z))) by Th1;
A19: [y,x] in [:C2,C1:] by A1, A15, ZFMISC_1:87;
reconsider y = y as set by TARSKI:1;
r = min (((converse g) . (z,y)),((converse f) . (y,x))) by A1, A2, A15, A16, Def2
.= min ((g . (y,z)),((converse f) . (y,x))) by A17, Def1
.= min ((g . (y,z)),(f . (x,y))) by A19, Def1
.= (min (f,g,x,z)) . y by A1, A2, A15, Def2 ;
hence (upper_bound (rng (min ((converse g),(converse f),z,x)))) - s <= upper_bound (rng (min (f,g,x,z))) by A14, A18, XXREAL_0:2; :: thesis: verum
end;
then upper_bound (rng (min ((converse g),(converse f),z,x))) <= upper_bound (rng (min (f,g,x,z))) by XREAL_1:57;
hence upper_bound (rng (min ((converse g),(converse f),z,x))) = upper_bound (rng (min (f,g,x,z))) by A11, XXREAL_0:1; :: thesis: verum