defpred S₁[ object , object ] means $2 = min ((h . [x,$1]),(g . [$1,z]));
A3: for y, c1, c2 being object st y in C2 & S₁[y,c1] & S₁[y,c2] holds
c1 = c2 ;
A4: for y, c being object st y in C2 & S₁[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 S₁[y,c] ) ) ) & ( for y being object st y in dom IT holds
S₁[y,IT . y] ) ) from PARTFUN1:sch 2(A4, A3);
A6: ( dom IT = C2 & rng IT c= [.0,1.] )

proof

C2 c= dom IT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in C2 or y in dom IT )
min ((h . [x,y]),(g . [y,z])) is set by TARSKI:1;
hence ( not y in C2 or y in dom IT ) by A5; :: thesis: verum

end;

hence dom IT = C2 by XBOOLE_0:def 10; :: thesis: rng IT c= [.0,1.]
reconsider A = [.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14;
let c be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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 b₁ being Membership_Func of C2 st
for y being Element of C2 holds b₁ . y = min ((h . [x,y]),(g . [y,z])) by A19; :: thesis: verum