let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for F being NAT -defined the Instructions of b₁ -valued FinPartState of holds IncAddr F,0 = F
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for F being NAT -defined the Instructions of S -valued FinPartState of holds IncAddr F,0 = F
let F be NAT -defined the Instructions of S -valued FinPartState of ; :: thesis: IncAddr F,0 = F
for m being natural number st m in dom F holds
F . m = IncAddr (F /. m),0

proof

let m be natural number ; :: thesis: ( m in dom F implies F . m = IncAddr (F /. m),0 )
assume m in dom F ; :: thesis: F . m = IncAddr (F /. m),0
then F /. m = F . m by PARTFUN1:def 8;
hence F . m = IncAddr (F /. m),0 by Th28; :: thesis: verum

end;

hence IncAddr F,0 = F by Def15; :: thesis: verum