let i be Element of NAT ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b₂ -valued Function
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p)
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 the Instructions of b₁ -valued Function
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p)
let S be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued Function
for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p)
let p be NAT -defined the Instructions of S -valued Function; :: thesis: for s1, s2 being State of S st p c= s1 & p c= s2 holds
(Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p)
let s1, s2 be State of S; :: thesis: ( p c= s1 & p c= s2 implies (Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p) )
assume that
A1: p c= s1 and
A2: p c= s2 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p)
set Cs2 = Comput ((ProgramPart s2),s2,i);
set Cs1 = Comput ((ProgramPart s1),s1,i);

A3: now

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

end;

dom (Comput ((ProgramPart s1),s1,i)) = the carrier of S by PARTFUN1:def 4
.= dom (Comput ((ProgramPart s2),s2,i)) by PARTFUN1:def 4 ;
hence (Comput ((ProgramPart s1),s1,i)) | (dom p) = (Comput ((ProgramPart s2),s2,i)) | (dom p) by A3, FUNCT_1:166; :: thesis: verum