defpred S₁[ set , set ] means $2 = max (h . $1),(g . $1);
A1: for x, y being set st x in C & S₁[x,y] holds
y in REAL ;
A2: for x, y1, y2 being set st x in C & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
consider IT being PartFunc of C, REAL such that
A3: ( ( for x being set holds
( x in dom IT iff ( x in C & ex y being set st S₁[x,y] ) ) ) & ( for x being set st x in dom IT holds
S₁[x,IT . x] ) ) from PARTFUN1:sch 2(A1, A2);
A4: ( dom IT = C & rng IT c= [.0 ,1.] )

proof

A5: dom IT = C

proof

C c= dom IT

proof

for x being set st x in C holds
x in dom IT

proof

let x be set ; :: thesis: ( x in C implies x in dom IT )
assume A6: x in C ; :: thesis: x in dom IT
ex y being set st y = max (h . x),(g . x) ;
hence x in dom IT by A3, A6; :: thesis: verum

end;

hence C c= dom IT by TARSKI:def 3; :: thesis: verum

end;

hence dom IT = C by XBOOLE_0:def 10; :: thesis: verum

end;

rng IT c= [.0 ,1.]

proof

A7: ( rng h c= [.0 ,1.] & rng g c= [.0 ,1.] ) by Def1;
for y being set st y in rng IT holds
y in [.0 ,1.]

proof

let y be set ; :: thesis: ( y in rng IT implies y in [.0 ,1.] )
assume y in rng IT ; :: thesis: y in [.0 ,1.]
then consider x being Element of C such that
A8: ( x in dom IT & y = IT . x ) by PARTFUN1:26;
reconsider A = [.0 ,1.] as closed-interval Subset of REAL by INTEGRA1:def 1;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then A9: ( 0 = lower_bound A & 1 = upper_bound A ) by INTEGRA1:6;
x in C ;
then ( x in dom h & x in dom g ) by Def1;
then ( h . x in rng h & g . x in rng g ) by FUNCT_1:def 5;
then ( 0 <= h . x & h . x <= 1 & 0 <= g . x & g . x <= 1 ) by A7, A9, INTEGRA2:1;
then ( 0 <= max (h . x),(g . x) & max (h . x),(g . x) <= 1 ) by XXREAL_0:28, XXREAL_0:30;
then ( 0 <= IT . x & IT . x <= 1 ) by A3, A8;
hence y in [.0 ,1.] by A8, A9, INTEGRA2:1; :: thesis: verum

end;

hence rng IT c= [.0 ,1.] by TARSKI:def 3; :: thesis: verum

end;

hence ( dom IT = C & rng IT c= [.0 ,1.] ) by A5; :: thesis: verum

end;

then A10: IT is Membership_Func of C by Def1;
for c being Element of C holds IT . c = max (h . c),(g . c) by A3, A4;
hence ex b₁ being Membership_Func of C st
for c being Element of C holds b₁ . c = max (h . c),(g . c) by A10; :: thesis: verum