defpred S1[ object , object ] means $2 = (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 = (h . c) * (g . c)
by A3;
A7:
rng g c= [.0,1.]
by RELAT_1:def 19;
A8:
rng h 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 A15:
0 <= h . x
by A8, A12, INTEGRA2:1;
A16:
1
= upper_bound A
by A11, INTEGRA1:5;
x in dom g
by A13, FUNCT_2:def 1;
then A17:
g . x in rng g
by FUNCT_1:def 3;
then A18:
g . x <= 1
by A7, A16, INTEGRA2:1;
0 <= g . x
by A7, A12, A17, INTEGRA2:1;
then
0 <= (h . x) * (g . x)
by A15, XREAL_1:127;
then A19:
0 <= IT . x
by A3, A9;
h . x <= 1
by A8, A16, A14, INTEGRA2:1;
then
(h . x) * (g . x) <= 1
by A15, A18, XREAL_1:160;
then
IT . x <= 1
by A3, A9;
hence
y in [.0,1.]
by A10, A12, A16, A19, INTEGRA2:1;
verum
end;
then
rng IT c= [.0,1.]
by TARSKI:def 3;
then
IT is Membership_Func of C
by A5, FUNCT_2:def 1, RELAT_1:def 19;
hence
ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = (h . c) * (g . c)
by A6; verum