defpred S1[ object ] means ex k being Element of NAT st $1 = 2 * k;
deffunc H1( object ) -> Element of S = b;
deffunc H2( object ) -> Element of S = a;
consider f being Function such that
A1: ( dom f = NAT & ( for x being object st x in NAT holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) ) ) from PARTFUN1:sch 1();
 A2: rng f c= {a,b}
proof
let x be object ; :: 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 object such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def 3;
per cases ( S1[y] or not S1[y] ) ;
end;
end;
for y being object st y in {a,b} holds
ex x being object st
( x in dom f & y = f . x )
proof
let y be object ; :: thesis: ( y in {a,b} implies ex x being object st
( x in dom f & y = f . x ) )
assume A5: y in {a,b} ; :: thesis: ex x being object 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 object st
( x in dom f & y = f . x )
take 2 ; :: thesis: ( 2 in dom f & y = f . 2 )
S1[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 object 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:9;
then rng f = {a,b} by A2;
then reconsider f = f as sequence of S by A1, FUNCT_2:def 1, RELSET_1:4;
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