let N be non empty with_non-empty_elements set ; :: thesis: for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds IC (p +* (Start-At (n,S))) = n
let n be Element of NAT ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being PartState of S holds IC (p +* (Start-At (n,S))) = n
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S holds IC (p +* (Start-At (n,S))) = n
let p be PartState of S; :: thesis: IC (p +* (Start-At (n,S))) = n
A1: IC S in dom (Start-At (n,S)) by Th52;
(Start-At (n,S)) . (IC S) = n by FUNCOP_1:87;
hence IC (p +* (Start-At (n,S))) = n by A1, FUNCT_4:14; :: thesis: verum