let i be Element of NAT ; :: 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 N
for p being NAT -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 N
for p being NAT -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 N; :: thesis: for p being NAT -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 NAT -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 that
A1: p c= s1 and
A2: p c= s2 ; :: thesis: (Computation s1,i) | (dom p) = (Computation s2,i) | (dom p)
set Cs2 = Computation s2,i;
set Cs1 = Computation s1,i;

A3: now

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

end;

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