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 steady-programmed definite AMI-Struct of N
for p being NAT -defined FinPartState of
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 steady-programmed definite AMI-Struct of N
for p being NAT -defined FinPartState of
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 steady-programmed definite AMI-Struct of N; :: thesis: for p being NAT -defined FinPartState of
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 FinPartState of ; :: 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