defpred S_{1}[ object , object ] means $2 = (h . $1) * (g . $1);

A1: for x, y1, y2 being object st x in C & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 ;

A2: for x, y being object st x in C & S_{1}[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 S_{1}[x,y] ) ) ) & ( for x being object st x in dom IT holds

S_{1}[x,IT . x] ) )
from PARTFUN1:sch 2(A2, A1);

for x being object st x in C holds

x in dom IT

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.]

then IT is Membership_Func of C by A5, FUNCT_2:def 1, RELAT_1:def 19;

hence ex b_{1} being Membership_Func of C st

for c being Element of C holds b_{1} . c = (h . c) * (g . c)
by A6; :: thesis: verum

A1: for x, y1, y2 being object st x in C & S

y1 = y2 ;

A2: for x, y being object st x in C & S

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 S

S

for x being object st x in C holds

x in dom IT

proof

then
C c= dom IT
by TARSKI:def 3;
let x be object ; :: thesis: ( x in C implies x in dom IT )

A4: ex y being set st y = (h . x) * (g . x) ;

assume x in C ; :: thesis: x in dom IT

hence x in dom IT by A3, A4; :: thesis: verum

end;A4: ex y being set st y = (h . x) * (g . x) ;

assume x in C ; :: thesis: x in dom IT

hence x in dom IT by A3, A4; :: thesis: verum

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

then
rng IT c= [.0,1.]
by TARSKI:def 3;
reconsider A = [.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14;

let y be object ; :: 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

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; :: thesis: verum

end;let y be object ; :: 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

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; :: thesis: verum

then IT is Membership_Func of C by A5, FUNCT_2:def 1, RELAT_1:def 19;

hence ex b

for c being Element of C holds b