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 s being State of S
for p being PartState of S st NPP (p +* (Start-At (n,S))) c= s holds
IC 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 s being State of S
for p being PartState of S st NPP (p +* (Start-At (n,S))) c= s holds
IC s = n
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for p being PartState of S st NPP (p +* (Start-At (n,S))) c= s holds
IC s = n
let s be State of S; :: thesis: for p being PartState of S st NPP (p +* (Start-At (n,S))) c= s holds
IC s = n
let p be PartState of S; :: thesis: ( NPP (p +* (Start-At (n,S))) c= s implies IC s = n )
assume A1: NPP (p +* (Start-At (n,S))) c= s ; :: thesis: IC s = n
A2: IC in dom (p +* (Start-At (n,S))) by Th141;
then IC in dom (NPP (p +* (Start-At (n,S)))) by Th179;
hence IC s = IC (NPP (p +* (Start-At (n,S)))) by A1, GRFUNC_1:8
.= IC (p +* (Start-At (n,S))) by Th72, A2
.= n by Th142 ;
:: thesis: verum