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 s being State of S
for p being NAT -defined PartState of
for k being Element of NAT holds
( p c= s iff p c= Comput (ProgramPart s),s,k )
let S be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for s being State of S
for p being NAT -defined PartState of
for k being Element of NAT holds
( p c= s iff p c= Comput (ProgramPart s),s,k )
let s be State of S; :: thesis: for p being NAT -defined PartState of
for k being Element of NAT holds
( p c= s iff p c= Comput (ProgramPart s),s,k )
let p be NAT -defined PartState of ; :: thesis: for k being Element of NAT holds
( p c= s iff p c= Comput (ProgramPart s),s,k )
let k be Element of NAT ; :: thesis: ( p c= s iff p c= Comput (ProgramPart s),s,k )
dom (Comput (ProgramPart s),s,k) = the carrier of S by PARTFUN1:def 4;
then A1: dom p c= dom (Comput (ProgramPart s),s,k) by RELAT_1:def 18;
A2: dom p c= NAT by RELAT_1:def 18;

A3: now

hereby :: thesis: ( ( for x being set st x in dom p holds
p . x = (Comput (ProgramPart s),s,k) . x ) implies for x being set st x in dom p holds
s . x = p . x )

assume A4: for x being set st x in dom p holds
p . x = s . x ; :: thesis: for x being set st x in dom p holds
(Comput (ProgramPart s),s,k) . x = p . x
let x be set ; :: thesis: ( x in dom p implies (Comput (ProgramPart s),s,k) . x = p . x )
assume A5: x in dom p ; :: thesis: (Comput (ProgramPart s),s,k) . x = p . x
then reconsider l = x as Element of NAT by A2;
thus (Comput (ProgramPart s),s,k) . x = s . l by Th54
.= p . x by A4, A5 ; :: thesis: verum

end;

assume A6: for x being set st x in dom p holds
p . x = (Comput (ProgramPart s),s,k) . x ; :: thesis: for x being set st x in dom p holds
s . x = p . x
let x be set ; :: thesis: ( x in dom p implies s . x = p . x )
assume A7: x in dom p ; :: thesis: s . x = p . x
then reconsider l = x as Element of NAT by A2;
thus s . x = (Comput (ProgramPart s),s,k) . l by Th54
.= p . x by A6, A7 ; :: thesis: verum

end;

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