set M = L \/ {(intloc 0)};
defpred S₁[ Element of omega ] 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();
not Int-Locations c= L \/ {(intloc 0)} by AMI_3:27;
then consider x being object such that
A2: x in Int-Locations and
A3: not x in L \/ {(intloc 0)} ;
reconsider x = x as Int-Location by A2, AMI_2:def 16;
consider k being Nat such that
A4: x = intloc k by SCMFSA_2:8;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
not intloc k in {(intloc 0)} by A3, A4, XBOOLE_0:def 3;
then A5: k <> 0 by TARSKI:def 1;
not intloc k in L by A3, A4, XBOOLE_0:def 3;
then k in { k where k is Element of NAT : S₁[k] } by A5;
then reconsider sn = { k where k is Element of NAT : S₁[k] } as non empty Subset of NAT by A1;
defpred S₂[ Nat, Subset of NAT, Subset of NAT] means for N being non empty Subset of NAT st N = $2 holds
$3 = $2 \ {(min N)};

A6: now :: thesis:

let n be 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 x9 = x as non empty Subset of NAT ;

now :: thesis:

reconsider mx9 = {(min x9)} as Subset of NAT ;
reconsider t = x9 \ mx9 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;

end;

end;

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

proof

deffunc H₁( Nat) -> Element of the carrier of SCM+FSA = intloc $1;
set Isn = { H₁(v) where v is Element of NAT : v in sn } ;
assume f . 0 is finite ; :: thesis:
then A10: sn is finite by A7;
{ H₁(v) where v is Element of NAT : v in sn } is finite from FRAENKEL:sch 21(A10);
then reconsider Isn = { H₁(v) where v is Element of NAT : v in sn } as finite set ;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

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

per cases by A11, XBOOLE_0:def 3;

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

hence x in Int-Locations ; :: thesis:

end;

suppose x in Isn ; :: thesis:

then ex k being Element of NAT st
( intloc k = x & k in sn ) ;
hence x in Int-Locations by AMI_2:def 16; :: thesis:

end;

end;

end;

assume x in Int-Locations ; :: thesis:
then reconsider x9 = x as Int-Location by AMI_2:def 16;
consider i being Nat such that
A12: x9 = intloc i by SCMFSA_2:8;

now :: thesis:

assume A13: not x in L \/ {(intloc 0)} ; :: thesis:
then not x9 in {(intloc 0)} by XBOOLE_0:def 3;
then A14: i <> 0 by A12, TARSKI:def 1;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
not intloc i in L by A12, A13, XBOOLE_0:def 3;
then i in sn by A14;
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 AMI_3:27, TARSKI:2; :: thesis:

end;

A15: for n being Nat st S₃[n] holds
S₃[n + 1]

proof

let n be Nat; :: thesis:
assume A16: f . n is infinite ; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider sn = f . nn as non empty Subset of NAT by A16;
min sn in sn by XXREAL_2:def 7;
then A17: {(min sn)} c= sn by ZFMISC_1:31;
assume f . (n + 1) is finite ; :: thesis:
then reconsider sn1 = f . (n + 1) as finite set ;
A18: sn1 \/ {(min sn)} is finite ;
f . (n + 1) = sn \ {(min sn)} by A8;
hence contradiction by A16, A17, A18, XBOOLE_1:45; :: thesis:

end;

thus for n being Nat holds S₃[n] from NAT_1:sch 2(A9, A15); :: thesis: