defpred S1[ object , object ] means $2 = min ((h . [x,$1]),(g . [$1,z]));
A3:
for y, c1, c2 being object st y in C2 & S1[y,c1] & S1[y,c2] holds
c1 = c2
;
A4:
for y, c being object st y in C2 & S1[y,c] holds
c in REAL
by XREAL_0:def 1;
consider IT being PartFunc of C2,REAL such that
A5:
( ( for y being object holds
( y in dom IT iff ( y in C2 & ex c being object st S1[y,c] ) ) ) & ( for y being object st y in dom IT holds
S1[y,IT . y] ) )
from PARTFUN1:sch 2(A4, A3);
A6:
( dom IT = C2 & rng IT c= [.0,1.] )
proof
C2 c= dom IT
hence
dom IT = C2
by XBOOLE_0:def 10;
rng IT c= [.0,1.]
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.] )
A8:
rng h c= [.0,1.]
by RELAT_1:def 19;
assume
c in rng IT
;
c in [.0,1.]
then consider y being
Element of
C2 such that A9:
y in dom IT
and A10:
c = IT . y
by PARTFUN1:3;
A11:
h . [x,y] >= min (
(h . [x,y]),
(g . [y,z]))
by XXREAL_0:17;
[x,y] in [:C1,C2:]
by A1, ZFMISC_1:87;
then
[x,y] in dom h
by FUNCT_2:def 1;
then A12:
h . [x,y] in rng h
by FUNCT_1:def 3;
[y,z] in [:C2,C3:]
by A2, ZFMISC_1:87;
then
[y,z] in dom g
by FUNCT_2:def 1;
then A13:
g . [y,z] in rng g
by FUNCT_1:def 3;
A14:
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A15:
0 = lower_bound A
by INTEGRA1:5;
A16:
1
= upper_bound A
by A14, INTEGRA1:5;
then
h . [x,y] <= 1
by A8, A12, INTEGRA2:1;
then
min (
(h . [x,y]),
(g . [y,z]))
<= 1
by A11, XXREAL_0:2;
then A17:
IT . y <= 1
by A5, A9;
rng g c= [.0,1.]
by RELAT_1:def 19;
then A18:
0 <= g . [y,z]
by A15, A13, INTEGRA2:1;
0 <= h . [x,y]
by A8, A15, A12, INTEGRA2:1;
then
0 <= min (
(h . [x,y]),
(g . [y,z]))
by A18, XXREAL_0:20;
then
0 <= IT . y
by A5, A9;
hence
c in [.0,1.]
by A10, A15, A16, A17, INTEGRA2:1;
verum
end;
then A19:
IT is Membership_Func of C2
by FUNCT_2:def 1, RELAT_1:def 19;
for y being Element of C2 holds IT . y = min ((h . [x,y]),(g . [y,z]))
by A5, A6;
hence
ex b1 being Membership_Func of C2 st
for y being Element of C2 holds b1 . y = min ((h . [x,y]),(g . [y,z]))
by A19; verum