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 NAT -defined PartState of
for P being the Instructions of b₁ -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput (P,s,k)
let S be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for p being NAT -defined PartState of
for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput (P,s,k)
let p be NAT -defined PartState of ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput (P,s,k)
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S st p c= s holds
for k being Element of NAT holds p c= Comput (P,s,k)
let s be State of S; :: thesis: ( p c= s implies for k being Element of NAT holds p c= Comput (P,s,k) )
assume A1: p c= s ; :: thesis: for k being Element of NAT holds p c= Comput (P,s,k)
let k be Element of NAT ; :: thesis: p c= Comput (P,s,k)
A2: dom p c= NAT by RELAT_1:def 18;

A3: now

let x be set ; :: thesis: ( x in dom p implies p . x = (Comput (P,s,k)) . x )
assume A4: x in dom p ; :: thesis: p . x = (Comput (P,s,k)) . x
then reconsider l = x as Element of NAT by A2;
s . x = (Comput (P,s,k)) . l by Th54;
hence p . x = (Comput (P,s,k)) . x by A1, A4, GRFUNC_1:8; :: thesis: verum

end;

dom s = the carrier of S by PARTFUN1:def 4
.= dom (Comput (P,s,k)) by PARTFUN1:def 4 ;
then dom p c= dom (Comput (P,s,k)) by A1, GRFUNC_1:8;
hence p c= Comput (P,s,k) by A3, GRFUNC_1:8; :: thesis: verum