defpred S₁[ set ] means $1 in dom h;
deffunc H₁( set ) -> Element of REAL = 1 - (h . $1);
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();
A2: ( dom IT = C & rng IT c= [.0 ,1.] )

proof

A3: dom IT = C

proof

C c= dom IT

proof

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 )
assume A4: x in C ; :: thesis: x in dom IT
dom h = C by Def1;
hence x in dom IT by A1, A4; :: thesis: verum

end;

hence C c= dom IT by TARSKI:def 3; :: thesis: verum

end;

hence dom IT = C by XBOOLE_0:def 10; :: thesis: verum

end;

rng IT c= [.0 ,1.]

proof

A5: rng h c= [.0 ,1.] by Def1;
for y being set st y in rng IT holds
y in [.0 ,1.]

proof

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

end;

hence rng IT c= [.0 ,1.] by TARSKI:def 3; :: thesis: verum

end;

hence ( dom IT = C & rng IT c= [.0 ,1.] ) by A3; :: thesis: verum

end;

then A9: IT is Membership_Func of C by Def1;
for c being Element of C holds IT . c = 1 - (h . c) by A1, A2;
hence ex b₁ being Membership_Func of C st
for c being Element of C holds b₁ . c = 1 - (h . c) by A9; :: thesis: verum