let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for l being Nat
for p being PartState of S
for s being State of S st p = (IC S),l --> l,(halt S) & p c= s holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = s
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N; :: thesis: for l being Nat
for p being PartState of S
for s being State of S st p = (IC S),l --> l,(halt S) & p c= s holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = s
let l be Nat; :: thesis: for p being PartState of S
for s being State of S st p = (IC S),l --> l,(halt S) & p c= s holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = s
set h = halt S;
let p be PartState of S; :: thesis: for s being State of S st p = (IC S),l --> l,(halt S) & p c= s holds
for i being Element of NAT holds Comput (ProgramPart s),s,i = s
let s be State of S; :: thesis: ( p = (IC S),l --> l,(halt S) & p c= s implies for i being Element of NAT holds Comput (ProgramPart s),s,i = s )
assume that
Z: p = (IC S),l --> l,(halt S) and
A3: p c= s ; :: thesis: for i being Element of NAT holds Comput (ProgramPart s),s,i = s
defpred S₁[ Element of NAT ] means Comput (ProgramPart s),s,$1 = s;

A4: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
ProgramPart (Comput (ProgramPart s),s,i) = ProgramPart s by LmA;
then Comput (ProgramPart s),s,(i + 1) = Following (ProgramPart (Comput (ProgramPart s),s,i)),(Comput (ProgramPart s),s,i) by Th14
.= Exec (halt S),s by Z, A3, A5, COMPOS_1:6
.= s by Def8 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ] by Th13;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A6, A4); :: thesis: verum