let n be Element of NAT ; :: thesis: ex N being Function of NAT,NAT st
( N . 0 = 1 & N . 1 = 2 & N . 2 = n )
defpred S₁[ set ] means $1 = 0 ;
deffunc H₁( set ) -> Element of NAT = 1;
deffunc H₂( set ) -> Element of NAT = 2;
consider N0 being Function such that
dom N0 = NAT and
A1: for i being set st i in NAT holds
( ( S₁[i] implies N0 . i = H₁(i) ) & ( not S₁[i] implies N0 . i = H₂(i) ) ) from PARTFUN1:sch 1();
defpred S₂[ set ] means $1 <> 2;
deffunc H₃( set ) -> set = N0 . $1;
deffunc H₄( set ) -> Element of NAT = n;
consider N being Function such that
A2: dom N = NAT and
A3: for i being set st i in NAT holds
( ( S₂[i] implies N . i = H₃(i) ) & ( not S₂[i] implies N . i = H₄(i) ) ) from PARTFUN1:sch 1();
rng N c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng N or x in NAT )
assume x in rng N ; :: thesis: x in NAT
then consider i being set such that
A4: i in dom N and
A5: x = N . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A2, A4;
( x = n or ( x = N0 . i & ( i = 0 or i <> 0 ) ) ) by A3, A5;
then ( x = n or x = 1 or x = 2 ) by A1;
hence x in NAT ; :: thesis: verum

end;

then reconsider N = N as Function of NAT,NAT by A2, FUNCT_2:2;
take N ; :: thesis: ( N . 0 = 1 & N . 1 = 2 & N . 2 = n )
A6: N . 0 = N0 . 0 by A3;
N0 . 1 = N . 1 by A3;
hence ( N . 0 = 1 & N . 1 = 2 ) by A1, A6; :: thesis: N . 2 = n
thus N . 2 = n by A3; :: thesis: verum