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 s being State of S
for p being programmed FinPartState of S
for k being Element of NAT holds
( p c= s iff 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 s being State of S
for p being programmed FinPartState of S
for k being Element of NAT holds
( p c= s iff 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 s being State of S
for p being programmed FinPartState of S
for k being Element of NAT holds
( p c= s iff p c= Computation s,k )
let s be State of S; :: thesis: for p being programmed FinPartState of S
for k being Element of NAT holds
( p c= s iff p c= Computation s,k )
let p be programmed FinPartState of S; :: thesis: for k being Element of NAT holds
( p c= s iff p c= Computation s,k )
let k be Element of NAT ; :: thesis: ( p c= s iff p c= Computation s,k )
( dom s = the carrier of S & dom (Computation s,k) = the carrier of S ) by Th79;
then A1: ( dom p c= dom s & dom p c= dom (Computation s,k) ) by Th80;
A2: dom p c= IL by Def40;

now

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

assume A3: 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
(Computation s,k) . x = p . x
let x be set ; :: thesis: ( x in dom p implies (Computation s,k) . x = p . x )
assume A4: x in dom p ; :: thesis: (Computation s,k) . x = p . x
then reconsider l = x as Instruction-Location of S by A2, Def4;
thus (Computation s,k) . x = s . l by Th54
.= p . x by A3, A4 ; :: thesis: verum

end;

assume A5: for x being set st x in dom p holds
p . x = (Computation 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 A6: x in dom p ; :: thesis: s . x = p . x
then reconsider l = x as Instruction-Location of S by A2, Def4;
thus s . x = (Computation s,k) . l by Th54
.= p . x by A5, A6 ; :: thesis: verum

end;

hence ( p c= s iff p c= Computation s,k ) by A1, GRFUNC_1:8; :: thesis: verum