defpred S₁[ Element of NAT ] means ( not intloc $1 in L & $1 <> 0 );
set sn = { k where k is Element of NAT : S₁[k] } ;
A1: { k where k is Element of NAT : S₁[k] } is Subset of NAT from DOMAIN_1:sch 7();
set M = L \/ {(intloc 0 )};
not Int-Locations c= L \/ {(intloc 0 )} ;
then consider x being set such that
A2: ( x in Int-Locations & not x in L \/ {(intloc 0 )} ) by TARSKI:def 3;
reconsider x = x as Int-Location by A2, SCMFSA_2:11;
consider k being Element of NAT such that
A3: x = intloc k by SCMFSA_2:19;
A4: ( not intloc k in L & not intloc k in {(intloc 0 )} ) by A2, A3, XBOOLE_0:def 3;
then k <> 0 by TARSKI:def 1;
then k in { k where k is Element of NAT : S₁[k] } by A4;
then reconsider sn = { k where k is Element of NAT : S₁[k] } as non empty Subset of NAT by A1;
defpred S₂[ Element of NAT , Subset of NAT , Subset of NAT ] means for N being non empty Subset of NAT st N = $2 holds
$3 = $2 \ {(min N)};

A5: now

let n be Element of NAT ; :: thesis:
let x be Subset of NAT ; :: thesis:

per cases ;

suppose x is empty ; :: thesis:

then S₂[n,x, {} NAT ] ;
hence ex y being Subset of NAT st S₂[n,x,y] ; :: thesis:

end;

suppose not x is empty ; :: thesis:

then reconsider x' = x as non empty Subset of NAT ;

reconsider mx' = {(min x')} as Subset of NAT by ZFMISC_1:37;
reconsider t = x' \ mx' as Subset of NAT ;
take t = t; :: thesis:
let N be non empty Subset of NAT ; :: thesis:
assume N = x ; :: thesis:
hence t = x \ {(min N)} ; :: thesis:

end;

hence ex y being Subset of NAT st S₂[n,x,y] ; :: thesis:

end;

consider f being Function of NAT ,(bool NAT ) such that
A6: f . 0 = sn and
A7: for n being Element of NAT holds S₂[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A5);
take f ; :: thesis:
thus f . 0 = { v where v is Element of NAT : ( not intloc v in L & v <> 0 ) } by A6; :: thesis:
thus for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} by A7; :: thesis:
defpred S₃[ Element of NAT ] means not f . $1 is finite ;
A8: S₃[ 0 ]

assume f . 0 is finite ; :: thesis:
then A9: sn is finite by A6;
deffunc H₁( Element of NAT ) -> Int-Location = intloc $1;
set Isn = { H₁(v) where v is Element of NAT : v in sn } ;
{ H₁(v) where v is Element of NAT : v in sn } is finite from FRAENKEL:sch 21(A9);
then reconsider Isn = { H₁(v) where v is Element of NAT : v in sn } as finite set ;

let x be set ; :: thesis:

hereby :: thesis:

assume A10: x in (L \/ {(intloc 0 )}) \/ Isn ; :: thesis:

per cases by A10, XBOOLE_0:def 3;

suppose x in L \/ {(intloc 0 )} ; :: thesis:

hence x in Int-Locations ; :: thesis:

end;

suppose x in Isn ; :: thesis:

then consider k being Element of NAT such that
A11: ( intloc k = x & k in sn ) ;
thus x in Int-Locations by A11, SCMFSA_2:def 4; :: thesis:

end;

assume x in Int-Locations ; :: thesis:
then reconsider x' = x as Int-Location by SCMFSA_2:11;
consider i being Element of NAT such that
A12: x' = intloc i by SCMFSA_2:19;

assume not x in L \/ {(intloc 0 )} ; :: thesis:
then ( not x' in L & not x' in {(intloc 0 )} ) by XBOOLE_0:def 3;
then ( not intloc i in L & i <> 0 ) by A12, TARSKI:def 1;
then i in sn ;
hence x in Isn by A12; :: thesis:

end;

hence x in (L \/ {(intloc 0 )}) \/ Isn by XBOOLE_0:def 3; :: thesis:

end;

hence contradiction by TARSKI:2; :: thesis:

end;

A13: for n being Element of NAT st S₃[n] holds
S₃[n + 1]

let n be Element of NAT ; :: thesis:
assume A14: not f . n is finite ; :: thesis:
then reconsider sn = f . n as non empty Subset of NAT ;
A15: f . (n + 1) = sn \ {(min sn)} by A7;
min sn in sn by XXREAL_2:def 7;
then A16: {(min sn)} c= sn by ZFMISC_1:37;
assume f . (n + 1) is finite ; :: thesis:
then reconsider sn1 = f . (n + 1) as finite set ;
sn1 \/ {(min sn)} is finite ;
hence contradiction by A14, A15, A16, XBOOLE_1:45; :: thesis:

end;

thus for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A8, A13); :: thesis: