defpred S₁[ object , object ] means $2 = ((h . $1) + (g . $1)) - ((h . $1) * (g . $1));
A1: for x, y1, y2 being object st x in C & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: for x, y being object st x in C & S₁[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₁[x,y] ) ) ) & ( for x being object st x in dom IT holds
S₁[x,IT . x] ) ) from PARTFUN1:sch 2(A2, A1);
for x being object st x in C holds
x in dom IT

proof

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

end;

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)) - ((h . c) * (g . c)) by A3;
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 ; :: 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
A7: x in dom IT and
A8: y = IT . x by PARTFUN1:3;
0 <= (1_minus h) . x by Th1;
then A9: 0 <= 1 - (h . x) by FUZZY_1:def 5;
(1_minus g) . x <= 1 by Th1;
then A10: 1 - (g . x) <= 1 by FUZZY_1:def 5;
(1_minus h) . x <= 1 by Th1;
then 1 - (h . x) <= 1 by FUZZY_1:def 5;
then (1 - (h . x)) * (1 - (g . x)) <= 1 by A9, A10, XREAL_1:160;
then 1 - ((1 - (h . x)) * (1 - (g . x))) >= 1 - 1 by XREAL_1:10;
then 0 <= ((h . x) + (g . x)) - ((h . x) * (g . x)) ;
then A11: 0 <= IT . x by A3, A7;
A12: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A13: 1 = upper_bound A by INTEGRA1:5;
0 <= (1_minus g) . x by Th1;
then 0 <= 1 - (g . x) by FUZZY_1:def 5;
then 0 <= (1 - (h . x)) * (1 - (g . x)) by A9, XREAL_1:127;
then 1 - 0 >= 1 - ((1 - (h . x)) * (1 - (g . x))) by XREAL_1:10;
then ((h . x) + (g . x)) - ((h . x) * (g . x)) <= 1 ;
then A14: IT . x <= 1 by A3, A7;
0 = lower_bound A by A12, INTEGRA1:5;
hence y in [.0,1.] by A8, A13, A11, A14, INTEGRA2:1; :: thesis: 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 b₁ being Membership_Func of C st
for c being Element of C holds b₁ . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) by A6; :: thesis: verum