let N be 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
X: i in NAT by ORDINAL1:def 13;
Y: dom s = the carrier of S by PARTFUN1:def 4;
NAT c= the carrier of S by Def3;
then i in the carrier of S by X;
then i in dom s by Y;
then i in dom (ProgramPart s) by X, RELAT_1:86;
hence (ProgramPart s) . i = s . i by FUNCT_1:70; :: thesis: verum