deffunc H₁( set ) -> Element of REAL = 1 - (h . $1);
defpred S₁[ set ] means $1 in dom h;
consider IT being PartFunc of C,REAL such that
A1: ( ( for x being Element of C holds
( x in dom IT iff S₁[x] ) ) & ( for x being Element of C st x in dom IT holds
IT . x = H₁(x) ) ) from SEQ_1:sch 3();
for x being set st x in C holds
x in dom IT

proof

let x be set ; :: thesis: ( x in C implies x in dom IT )
A2: dom h = C by FUNCT_2:def 1;
assume x in C ; :: thesis: x in dom IT
hence x in dom IT by A1, A2; :: thesis: verum

end;

then C c= dom IT by TARSKI:def 3;
then A3: dom IT = C by XBOOLE_0:def 10;
then A4: for c being Element of C holds IT . c = 1 - (h . c) by A1;
A5: rng h c= [.0 ,1.] by RELAT_1:def 19;
for y being set st y in rng IT holds
y in [.0 ,1.]

proof

reconsider A = [.0 ,1.] as closed-interval Subset of REAL by INTEGRA1:def 1;
let y be set ; :: 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
A6: x in dom IT and
A7: y = IT . x by PARTFUN1:26;
A8: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then A9: 0 = lower_bound A by INTEGRA1:6;
x in C ;
then x in dom h by FUNCT_2:def 1;
then A10: h . x in rng h by FUNCT_1:def 5;
then 0 <= h . x by A5, A9, INTEGRA2:1;
then 0 + 1 <= 1 + (h . x) by XREAL_1:8;
then 1 - (h . x) <= 1 by XREAL_1:22;
then A11: IT . x <= 1 by A1, A6;
A12: 1 = upper_bound A by A8, INTEGRA1:6;
then h . x <= 1 by A5, A10, INTEGRA2:1;
then 0 <= 1 - (h . x) by XREAL_1:50;
then 0 <= IT . x by A1, A6;
hence y in [.0 ,1.] by A7, A9, A12, A11, INTEGRA2:1; :: thesis: verum

end;

then A13: rng IT c= [.0 ,1.] by TARSKI:def 3;
IT is total by A3, PARTFUN1:def 4;
then IT is Membership_Func of C by A13, RELAT_1:def 19;
hence ex b₁ being Membership_Func of C st
for c being Element of C holds b₁ . c = 1 - (h . c) by A4; :: thesis: verum