deffunc H1( object ) -> set = { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = $1 & x0 <= y ) } ;
A1: now :: thesis: for x being object st x in NAT holds
H1(x) in bool NAT
let x be object ; :: thesis: ( x in NAT implies H1(x) in bool NAT )
assume x in NAT ; :: thesis: H1(x) in bool NAT
now :: thesis: for t being object st t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } holds
t in NAT
let t be object ; :: thesis: ( t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } implies t in NAT )
assume t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } ; :: thesis: t in NAT
then consider y0 being Element of NAT such that
A2: t = y0 and
ex x0 being Element of NAT st
( x0 = x & x0 <= y0 ) ;
thus t in NAT by A2; :: thesis: verum
end;
then { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } c= NAT ;
hence H1(x) in bool NAT ; :: thesis: verum
end;
ex f being Function of NAT,(bool NAT) st
for x being object st x in NAT holds
f . x = H1(x) from FUNCT_2:sch 2(A1);
 then consider F being Function of NAT,(bool NAT) such that
A3: for x being object st x in NAT holds
F . x = H1(x) ;
for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y }
proof
let x be Element of NAT ; :: thesis: F . x = { y where y is Element of NAT : x <= y }
{ y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } = { y where y is Element of NAT : x <= y }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { y where y is Element of NAT : x <= y } c= { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) }
let t be object ; :: thesis: ( t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } implies t in { y where y is Element of NAT : x <= y } )
assume t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } ; :: thesis: t in { y where y is Element of NAT : x <= y }
then consider y0 being Element of NAT such that
A4: t = y0 and
A5: ex x0 being Element of NAT st
( x0 = x & x0 <= y0 ) ;
consider x1 being Element of NAT such that
A6: x1 = x and
A7: x1 <= y0 by A5;
thus t in { y where y is Element of NAT : x <= y } by A4, A6, A7; :: thesis: verum
end;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Element of NAT : x <= y } or t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } )
assume t in { y where y is Element of NAT : x <= y } ; :: thesis: t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) }
then consider y0 being Element of NAT such that
A8: t = y0 and
A9: x <= y0 ;
thus t in { y where y is Element of NAT : ex x0 being Element of NAT st
( x0 = x & x0 <= y ) } by A8, A9; :: thesis: verum
end;
hence F . x = { y where y is Element of NAT : x <= y } by A3; :: thesis: verum
end;
hence ex F being sequence of (bool NAT) st
for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } ; :: thesis: verum