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