let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (ProgramPart s),s,i
let S be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for p being PartState of S
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (ProgramPart s),s,i
let p be PartState of S; :: thesis: for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (ProgramPart s),s,i
let s be State of S; :: thesis: ( p c= s implies for i being Element of NAT holds ProgramPart p c= Comput (ProgramPart s),s,i )
assume A1: p c= s ; :: thesis: for i being Element of NAT holds ProgramPart p c= Comput (ProgramPart s),s,i
let i be Element of NAT ; :: thesis: ProgramPart p c= Comput (ProgramPart s),s,i
ProgramPart p c= p by RELAT_1:88;
then ProgramPart p c= s by A1, XBOOLE_1:1;
hence ProgramPart p c= Comput (ProgramPart s),s,i by Th81; :: thesis: verum