let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N; :: thesis: for s being State of S
for i being natural number holds (ProgramPart s) /. i = s . i
let s be State of S; :: thesis: for i being natural number holds (ProgramPart s) /. i = s . i
let i be natural number ; :: thesis: (ProgramPart s) /. i = s . i
dom (ProgramPart s) = NAT by LmU;
then i in dom (ProgramPart s) by ORDINAL1:def 13;
hence (ProgramPart s) /. i = (ProgramPart s) . i by PARTFUN1:def 8
.= s . i by BWL ;
:: thesis: verum