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 PartState of S
for i being natural number st i in dom s 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 PartState of S
for i being natural number st i in dom s holds
(ProgramPart s) . i = s . i
let s be PartState of S; :: thesis: for i being natural number st i in dom s holds
(ProgramPart s) . i = s . i
let i be natural number ; :: thesis: ( i in dom s implies (ProgramPart s) . i = s . i )
assume Z: i in dom s ; :: thesis: (ProgramPart s) . i = s . i
X: i in NAT by ORDINAL1:def 13;
i in dom (ProgramPart s) by X, Z, RELAT_1:86;
hence (ProgramPart s) . i = s . i by FUNCT_1:70; :: thesis: verum