let i be Element of NAT ; :: thesis: for IL being non empty set
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 b₁ -defined FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
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 IL -defined FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
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 IL -defined FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of IL,N; :: thesis: for p being IL -defined FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
let p be IL -defined FinPartState of S; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies (Computation s1,i) | (dom p) = (Computation s2,i) | (dom p) )
assume A1: ( p c= s1 & p c= s2 ) ; :: thesis: (Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
set Cs1 = Computation s1,i;
set Cs2 = Computation s2,i;

A2: now

let x be set ; :: thesis: ( x in dom p implies (Computation s1,i) . x = (Computation s2,i) . x )
assume A3: x in dom p ; :: thesis: (Computation s1,i) . x = (Computation s2,i) . x
dom p c= IL by RELAT_1:def 18;
then reconsider l = x as Instruction-Location of S by A3, Def4;
A4: s1 . l = (Computation s1,i) . l by Th54;
A5: s2 . l = (Computation s2,i) . l by Th54;
p . x = s1 . x by A1, A3, GRFUNC_1:8;
hence (Computation s1,i) . x = (Computation s2,i) . x by A1, A3, A4, A5, GRFUNC_1:8; :: thesis: verum

end;

dom (Computation s1,i) = the carrier of S by Th79
.= dom (Computation s2,i) by Th79 ;
hence (Computation s1,i) | (dom p) = (Computation s2,i) | (dom p) by A2, FUNCT_1:166; :: thesis: verum