defpred S1[ object , object , object ] means $3 = upper_bound (rng (min (h,g,$1,$2)));
A1:
for x, z, c1, c2 being object st x in C1 & z in C3 & S1[x,z,c1] & S1[x,z,c2] holds
c1 = c2
;
A2:
for x, z, c being object st x in C1 & z in C3 & S1[x,z,c] holds
c in REAL
by XREAL_0:def 1;
consider IT being PartFunc of [:C1,C3:],REAL such that
A3:
( ( for x, z being object holds
( [x,z] in dom IT iff ( x in C1 & z in C3 & ex c being object st S1[x,z,c] ) ) ) & ( for x, z being object st [x,z] in dom IT holds
S1[x,z,IT . (x,z)] ) )
from BINOP_1:sch 5(A2, A1);
[:C1,C3:] c= dom IT
proof
let x,
z be
object ;
RELAT_1:def 3 ( not [x,z] in [:C1,C3:] or [x,z] in dom IT )
A5:
upper_bound (rng (min (h,g,x,z))) is
set
by TARSKI:1;
assume A6:
[x,z] in [:C1,C3:]
;
[x,z] in dom IT
then A7:
z in C3
by ZFMISC_1:87;
x in C1
by A6, ZFMISC_1:87;
hence
[x,z] in dom IT
by A3, A5, A7;
verum
end;
then A8:
dom IT = [:C1,C3:]
;
rng IT c= [.0,1.]
proof
reconsider A =
[.0,jj.] as non
empty closed_interval Subset of
REAL by MEASURE5:14;
let c be
object ;
TARSKI:def 3 ( not c in rng IT or c in [.0,1.] )
assume
c in rng IT
;
c in [.0,1.]
then consider a being
Element of
[:C1,C3:] such that
a in dom IT
and A10:
c = IT . a
by PARTFUN1:3;
A11:
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A12:
0 = lower_bound A
by INTEGRA1:5;
A13:
for
x,
z being
set holds
(
0 <= upper_bound (rng (min (h,g,x,z))) &
upper_bound (rng (min (h,g,x,z))) <= 1 )
proof
let x,
z be
set ;
( 0 <= upper_bound (rng (min (h,g,x,z))) & upper_bound (rng (min (h,g,x,z))) <= 1 )
A14:
rng (min (h,g,x,z)) c= A
by RELAT_1:def 19;
A is
bounded_below
by INTEGRA1:3;
then A15:
lower_bound A <= lower_bound (rng (min (h,g,x,z)))
by A14, SEQ_4:47;
A is
bounded_above
by INTEGRA1:3;
then A16:
upper_bound (rng (min (h,g,x,z))) <= upper_bound A
by A14, SEQ_4:48;
lower_bound (rng (min (h,g,x,z))) <= upper_bound (rng (min (h,g,x,z)))
by Th1, SEQ_4:11;
hence
(
0 <= upper_bound (rng (min (h,g,x,z))) &
upper_bound (rng (min (h,g,x,z))) <= 1 )
by A11, A16, A15, INTEGRA1:5;
verum
end;
consider x,
z being
object such that
x in C1
and
z in C3
and A17:
a = [x,z]
by ZFMISC_1:def 2;
reconsider z =
z,
x =
x as
set by TARSKI:1;
A18:
IT . (
x,
z)
= upper_bound (rng (min (h,g,x,z)))
by A3, A8, A17;
then A19:
IT . a <= 1
by A13, A17;
A20:
1
= upper_bound A
by A11, INTEGRA1:5;
0 <= IT . a
by A13, A17, A18;
hence
c in [.0,1.]
by A10, A12, A20, A19, INTEGRA2:1;
verum
end;
then
IT is RMembership_Func of C1,C3
by A8, FUNCT_2:def 1, RELAT_1:def 19;
hence
ex b1 being RMembership_Func of C1,C3 st
for x, z being object st [x,z] in [:C1,C3:] holds
b1 . (x,z) = upper_bound (rng (min (h,g,x,z)))
by A3, A8; verum