let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l being Nat
for I being Instruction of S
for P being NAT -defined the InstructionsF of b1 -valued Function st l .--> I c= P holds
for s being State of S st () .--> l c= s holds
CurInstr (P,s) = I

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for l being Nat
for I being Instruction of S
for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st () .--> l c= s holds
CurInstr (P,s) = I

let l be Nat; :: thesis: for I being Instruction of S
for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st () .--> l c= s holds
CurInstr (P,s) = I

let I be Instruction of S; :: thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st () .--> l c= s holds
CurInstr (P,s) = I

let P be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( l .--> I c= P implies for s being State of S st () .--> l c= s holds
CurInstr (P,s) = I )

assume A1: l .--> I c= P ; :: thesis: for s being State of S st () .--> l c= s holds
CurInstr (P,s) = I

let s be State of S; :: thesis: ( () .--> l c= s implies CurInstr (P,s) = I )
assume A2: (IC ) .--> l c= s ; :: thesis: CurInstr (P,s) = I
IC in dom (() .--> l) by TARSKI:def 1;
then A3: IC s = (() .--> l) . () by
.= l by FUNCOP_1:72 ;
A4: IC s in dom (l .--> I) by ;
dom (l .--> I) c= dom P by ;
hence CurInstr (P,s) = P . (IC s) by
.= (l .--> I) . (IC s) by
.= I by ;
:: thesis: verum