defpred S₁[ set ] means ex k being Element of NAT st $1 = 2 * k;
deffunc H₁( set ) -> Element of S = b;
deffunc H₂( set ) -> Element of S = a;
consider f being Function such that
A1: ( dom f = NAT & ( for x being set st x in NAT holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) ) ) from PARTFUN1:sch 1();
A2: rng f c= {a,b}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in {a,b} )
assume x in rng f ; :: thesis: x in {a,b}
then consider y being set such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 5;

per cases ( S₁[y] or not S₁[y] ) ;

suppose S₁[y] ; :: thesis: x in {a,b}

then f . y = a by A1;
hence x in {a,b} by A4, TARSKI:def 2; :: thesis: verum

end;

suppose not S₁[y] ; :: thesis: x in {a,b}

then f . y = b by A1, A3;
hence x in {a,b} by A4, TARSKI:def 2; :: thesis: verum

end;

end;

end;

for y being set st y in {a,b} holds
ex x being set st
( x in dom f & y = f . x )

proof

let y be set ; :: thesis: ( y in {a,b} implies ex x being set st
( x in dom f & y = f . x ) )
assume A5: y in {a,b} ; :: thesis: ex x being set st
( x in dom f & y = f . x )

per cases ( y = a or y = b ) by A5, TARSKI:def 2;

suppose A6: y = a ; :: thesis: ex x being set st
( x in dom f & y = f . x )

take 2 ; :: thesis: ( 2 in dom f & y = f . 2 )
S₁[2]

proof

take 1 ; :: thesis: 2 = 2 * 1
thus 2 = 2 * 1 ; :: thesis: verum

end;

hence ( 2 in dom f & y = f . 2 ) by A1, A6; :: thesis: verum

end;

suppose A7: y = b ; :: thesis: ex x being set st
( x in dom f & y = f . x )

take 1 ; :: thesis: ( 1 in dom f & y = f . 1 )
for k being Element of NAT holds 1 <> 2 * k by NAT_1:15;
hence ( 1 in dom f & y = f . 1 ) by A1, A7; :: thesis: verum

end;

end;

end;

then {a,b} c= rng f by FUNCT_1:19;
then rng f = {a,b} by A2, XBOOLE_0:def 10;
then reconsider f = f as Function of NAT ,S by A1, FUNCT_2:def 1, RELSET_1:11;
take f ; :: thesis: for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) )
let i be Element of NAT ; :: thesis: ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) )
thus ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) ) by A1; :: thesis: verum