let z be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for l being Element of NAT
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
let N be non empty with_non-empty_elements set ; :: thesis: for l being Element of NAT
for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
let l be Element of NAT ; :: thesis: for i being Element of the Instructions of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
let i be Element of the Instructions of (STC N); :: thesis: ( l = z & InsCode i = 1 implies NIC (i,l) = {(z + 1)} )
assume that
A1: l = z and
A2: InsCode i = 1 ; :: thesis: NIC (i,l) = {(z + 1)}
set M = STC N;
set F = { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } ;

now

set f = NAT --> i;
consider w being State of (STC N);
reconsider l9 = l as Element of ObjectKind (IC (STC N)) by COMPOS_1:def 6;
set u = (IC (STC N)) .--> l9;
A4: dom ((IC (STC N)) .--> l9) = {(IC (STC N))} by FUNCOP_1:19;
reconsider s = w +* (NAT --> i) as State of (STC N) ;
let y be set ; :: thesis: ( ( y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } implies y in {(z + 1)} ) & ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } ) )
A5: dom (NAT --> i) = NAT by FUNCOP_1:19;
reconsider t = s +* ((IC (STC N)) .--> l9) as Element of product the Object-Kind of (STC N) by PBOOLE:155;
l <> IC (STC N) by COMPOS_1:3;
then X: not l in dom ((IC (STC N)) .--> l9) by A4, TARSKI:def 1;
A6: (ProgramPart t) /. l = t . l by COMPOS_1:38
.= s . l by X, FUNCT_4:12
.= (NAT --> i) . l by A5, FUNCT_4:14
.= i by FUNCOP_1:13 ;

hereby :: thesis: ( y in {(z + 1)} implies y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } )

assume y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } ; :: thesis: y in {(z + 1)}
then ex s being Element of product the Object-Kind of (STC N) st
( y = IC (Exec (i,s)) & IC s = l ) ;
then y = succ z by A1, A2, Lm4
.= z + 1 ;
hence y in {(z + 1)} by TARSKI:def 1; :: thesis: verum

end;

assume y in {(z + 1)} ; :: thesis: y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l }
then A7: y = z + 1 by TARSKI:def 1
.= succ z ;
IC (STC N) in dom ((IC (STC N)) .--> l9) by A4, TARSKI:def 1;
then A8: IC t = ((IC (STC N)) .--> l9) . (IC (STC N)) by FUNCT_4:14
.= z by A1, FUNCOP_1:87 ;
then IC (Following ((ProgramPart t),t)) = succ z by A1, A2, A6, Lm4;
hence y in { (IC (Exec (i,ss))) where ss is Element of product the Object-Kind of (STC N) : IC ss = l } by A1, A7, A8, A6; :: thesis: verum

end;

hence NIC (i,l) = {(z + 1)} by TARSKI:2; :: thesis: verum