defpred S_{1}[ object ] means ex k being Element of NAT st $1 = 2 * k;

deffunc H_{1}( object ) -> Element of S = b;

deffunc H_{2}( object ) -> Element of S = a;

consider f being Function such that

A1: ( dom f = NAT & ( for x being object st x in NAT holds

( ( S_{1}[x] implies f . x = H_{2}(x) ) & ( not S_{1}[x] implies f . x = H_{1}(x) ) ) ) )
from PARTFUN1:sch 1();

A2: rng f c= {a,b}

ex x being object st

( x in dom f & y = f . x )

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

deffunc H

deffunc H

consider f being Function such that

A1: ( dom f = NAT & ( for x being object st x in NAT holds

( ( S

A2: rng f c= {a,b}

proof

for y being object st y in {a,b} holds
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;

end;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
( S_{1}[y] or not S_{1}[y] )
;

end;

end;

ex x being object st

( x in dom f & y = f . x )

proof

then
{a,b} c= rng f
by FUNCT_1:9;
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 )

end;( 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 )

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