let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
let f be RMembership_Func of C2,C3; :: thesis: for x, z being set st x in C1 & z in C3 holds
upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
let x, z be set ; :: thesis: ( x in C1 & z in C3 implies upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z] )
assume that
A1: x in C1 and
A2: z in C3 ; :: thesis: upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z]
rng (min ((Zmf (C1,C2)),f,x,z)) is real-bounded by Th1;
then A3: rng (min ((Zmf (C1,C2)),f,x,z)) is bounded_above by XXREAL_2:def 11;
for s being Real st 0 < s holds
(upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z]

proof

let s be Real; :: thesis: ( 0 < s implies (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z] )
assume s > 0 ; :: thesis: (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z]
then consider r being Real such that
A4: r in rng (min ((Zmf (C1,C2)),f,x,z)) and
A5: (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s < r by A3, SEQ_4:def 1;
consider y being object such that
A6: y in dom (min ((Zmf (C1,C2)),f,x,z)) and
A7: r = (min ((Zmf (C1,C2)),f,x,z)) . y by A4, FUNCT_1:def 3;
A8: [x,y] in [:C1,C2:] by A1, A6, ZFMISC_1:87;
A9: [x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
A10: 0 <= f . [y,z] by Th3;
r = min (((Zmf (C1,C2)) . [x,y]),(f . [y,z])) by A1, A2, A6, A7, Def2
.= min (0,(f . [y,z])) by A8, FUNCT_3:def 3
.= 0 by A10, XXREAL_0:def 9
.= (Zmf (C1,C3)) . [x,z] by A9, FUNCT_3:def 3 ;
hence (upper_bound (rng (min ((Zmf (C1,C2)),f,x,z)))) - s <= (Zmf (C1,C3)) . [x,z] by A5; :: thesis: verum

end;

then A11: upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) <= (Zmf (C1,C3)) . [x,z] by XREAL_1:57;
upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) >= (Zmf (C1,C3)) . [x,z]

proof

reconsider A = [.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A is bounded_below by INTEGRA1:3;
rng (min ((Zmf (C1,C2)),f,x,z)) c= [.0,1.] by RELAT_1:def 19;
then A13: lower_bound A <= lower_bound (rng (min ((Zmf (C1,C2)),f,x,z))) by A12, SEQ_4:47;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A14: 0 = lower_bound A by INTEGRA1:5;
A15: lower_bound (rng (min ((Zmf (C1,C2)),f,x,z))) <= upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) by Th1, SEQ_4:11;
[x,z] in [:C1,C3:] by A1, A2, ZFMISC_1:87;
hence upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) >= (Zmf (C1,C3)) . [x,z] by A14, A13, A15, FUNCT_3:def 3; :: thesis: verum

end;

hence upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) = (Zmf (C1,C3)) . [x,z] by A11, XXREAL_0:1; :: thesis: verum