let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for p being programmed FinPartState of S
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Computation s,k
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N
for p being programmed FinPartState of S
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Computation s,k
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N; :: thesis: for p being programmed FinPartState of S
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Computation s,k
let p be programmed FinPartState of S; :: thesis: for s being State of S st p c= s holds
for k being Element of NAT holds p c= Computation s,k
let s be State of S; :: thesis: ( p c= s implies for k being Element of NAT holds p c= Computation s,k )
assume A1: p c= s ; :: thesis: for k being Element of NAT holds p c= Computation s,k
let k be Element of NAT ; :: thesis: p c= Computation s,k
dom s = the carrier of S by Th79
.= dom (Computation s,k) by Th79 ;
then A2: dom p c= dom (Computation s,k) by A1, GRFUNC_1:8;
A3: dom p c= IL by Def40;

now

let x be set ; :: thesis: ( x in dom p implies p . x = (Computation s,k) . x )
assume A4: x in dom p ; :: thesis: p . x = (Computation s,k) . x
then reconsider l = x as Instruction-Location of S by A3, Def4;
s . x = (Computation s,k) . l by Th54;
hence p . x = (Computation s,k) . x by A1, A4, GRFUNC_1:8; :: thesis: verum

end;

hence p c= Computation s,k by A2, GRFUNC_1:8; :: thesis: verum