defpred S1[ object , object ] means $2 = max ((h . $1),(g . $1));
A1:
for x, y1, y2 being object st x in C & S1[x,y1] & S1[x,y2] holds
y1 = y2
;
A2:
for x, y being object st x in C & S1[x,y] holds
y in REAL
by XREAL_0:def 1;
consider IT being PartFunc of C,REAL such that
A3:
( ( for x being object holds
( x in dom IT iff ( x in C & ex y being object st S1[x,y] ) ) ) & ( for x being object st x in dom IT holds
S1[x,IT . x] ) )
from PARTFUN1:sch 2(A2, A1);
for x being object st x in C holds
x in dom IT
then
C c= dom IT
by TARSKI:def 3;
then A5:
dom IT = C
by XBOOLE_0:def 10;
then A6:
for c being Element of C holds IT . c = max ((h . c),(g . c))
by A3;
A7:
rng h c= [.0,1.]
by RELAT_1:def 19;
A8:
rng g c= [.0,1.]
by RELAT_1:def 19;
for y being object st y in rng IT holds
y in [.0,1.]
proof
reconsider A =
[.0,jj.] as non
empty closed_interval Subset of
REAL by MEASURE5:14;
let y be
object ;
( y in rng IT implies y in [.0,1.] )
assume
y in rng IT
;
y in [.0,1.]
then consider x being
Element of
C such that A9:
x in dom IT
and A10:
y = IT . x
by PARTFUN1:3;
A11:
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then A12:
0 = lower_bound A
by INTEGRA1:5;
A13:
x in C
;
then
x in dom h
by FUNCT_2:def 1;
then A14:
h . x in rng h
by FUNCT_1:def 3;
then
0 <= h . x
by A7, A12, INTEGRA2:1;
then
0 <= max (
(h . x),
(g . x))
by XXREAL_0:30;
then A15:
0 <= IT . x
by A3, A9;
A16:
1
= upper_bound A
by A11, INTEGRA1:5;
x in dom g
by A13, FUNCT_2:def 1;
then
g . x in rng g
by FUNCT_1:def 3;
then A17:
g . x <= 1
by A8, A16, INTEGRA2:1;
h . x <= 1
by A7, A16, A14, INTEGRA2:1;
then
max (
(h . x),
(g . x))
<= 1
by A17, XXREAL_0:28;
then
IT . x <= 1
by A3, A9;
hence
y in [.0,1.]
by A10, A12, A16, A15, INTEGRA2:1;
verum
end;
then A18:
rng IT c= [.0,1.]
by TARSKI:def 3;
IT is total
by A5, PARTFUN1:def 2;
then
IT is Membership_Func of C
by A18, RELAT_1:def 19;
hence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = max ((h . c),(g . c))
by A6; verum