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 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 )
|.((h . x) - (g . x)).| is set by TARSKI:1;
hence ( x in C implies x in dom IT ) by A3; :: 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)).| 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 ; :: 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;
0 <= |.((h . x) - (g . x)).| by COMPLEX1:46;
then A11: 0 <= IT . x by A3, A9;
A12: A = [.(),().] by INTEGRA1:4;
then A13: 0 = lower_bound A by INTEGRA1:5;
A14: x in C ;
then x in dom h by FUNCT_2:def 1;
then A15: h . x in rng h by FUNCT_1:def 3;
x in dom g by ;
then A16: g . x in rng g by FUNCT_1:def 3;
then 0 <= g . x by ;
then A17: 1 - 0 >= 1 - (g . x) by XREAL_1:10;
A18: 1 = upper_bound A by ;
then g . x <= 1 by ;
then A19: - (g . x) >= - 1 by XREAL_1:24;
0 <= h . x by ;
then 0 - (g . x) <= (h . x) - (g . x) by XREAL_1:9;
then A20: - 1 <= (h . x) - (g . x) by ;
h . x <= 1 by ;
then (h . x) - (g . x) <= 1 - (g . x) by XREAL_1:9;
then (h . x) - (g . x) <= 1 by ;
then |.((h . x) - (g . x)).| <= 1 by ;
then IT . x <= 1 by A3, A9;
hence y in [.0,1.] by ; :: thesis: verum
end;
then A21: rng IT c= [.0,1.] by TARSKI:def 3;
IT is total by ;
then IT is Membership_Func of C by ;
hence ex b1 being Membership_Func of C st
for c being Element of C holds b1 . c = |.((h . c) - (g . c)).| by A6; :: thesis: verum