let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for p being FinPartState of S
for s1, s2 being State of S st p c= s1 & Relocated (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N; :: thesis: for k being Element of NAT
for p being FinPartState of S
for s1, s2 being State of S st p c= s1 & Relocated (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let k be Element of NAT ; :: thesis: for p being FinPartState of S
for s1, s2 being State of S st p c= s1 & Relocated (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let p be FinPartState of S; :: thesis: for s1, s2 being State of S st p c= s1 & Relocated (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of S; :: thesis: ( p c= s1 & Relocated (p,k) c= s2 implies p c= s1 +* (DataPart s2) )
assume that
A1: p c= s1 and
A2: Relocated (p,k) c= s2 ; :: thesis: p c= s1 +* (DataPart s2)
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of S ;
A3: dom p c= the carrier of S by RELAT_1:def 18;
then A4: dom p c= ({(IC )} \/ (Data-Locations S)) \/ NAT by Th160;

A5: now

Data-Locations S = (dom s2) /\ (Data-Locations S) by Th49, XBOOLE_1:28;
then A6: dom (DataPart s2) = Data-Locations S by RELAT_1:90;
let x be set ; :: thesis: ( x in dom p implies p . b₁ = s . b₁ )
assume A7: x in dom p ; :: thesis: p . b₁ = s . b₁
A8: ( x in {(IC )} \/ (Data-Locations S) or x in NAT ) by A4, A7, XBOOLE_0:def 3;

per cases ( x in {(IC )} or x in Data-Locations S or x in NAT ) by A8, XBOOLE_0:def 3;

suppose A9: x in {(IC )} ; :: thesis: p . b₁ = s . b₁

A10: not IC in Data-Locations S by Th56;
x = IC by A9, TARSKI:def 1;
then s1 . x = s . x by A6, A10, FUNCT_4:12;
hence p . x = s . x by A1, A7, GRFUNC_1:8; :: thesis: verum

end;

suppose A11: x in Data-Locations S ; :: thesis: p . b₁ = s . b₁

set DPp = DataPart p;
x in (dom p) /\ (Data-Locations S) by A7, A11, XBOOLE_0:def 4;
then A12: x in dom (DataPart p) by RELAT_1:90;
DataPart p = DataPart (Relocated (p,k)) by Th115;
then DataPart p c= Relocated (p,k) by RELAT_1:88;
then A13: DataPart p c= s2 by A2, XBOOLE_1:1;
then dom (DataPart p) c= dom s2 by GRFUNC_1:8;
then x in (dom s2) /\ (Data-Locations S) by A11, A12, XBOOLE_0:def 4;
then A14: x in dom (DataPart s2) by RELAT_1:90;
DataPart p c= p by RELAT_1:88;
then A15: (DataPart p) . x = p . x by A12, GRFUNC_1:8;
A16: s2 . x = (DataPart s2) . x by A11, FUNCT_1:72;
(DataPart p) . x = s2 . x by A12, A13, GRFUNC_1:8;
hence p . x = s . x by A15, A16, A14, FUNCT_4:14; :: thesis: verum

end;

suppose A17: x in NAT ; :: thesis: p . b₁ = s . b₁

dom (DataPart s2) misses NAT by Th137;
then not x in dom (DataPart s2) by A17, XBOOLE_0:3;
then s1 . x = s . x by FUNCT_4:12;
hence p . x = s . x by A1, A7, GRFUNC_1:8; :: thesis: verum

end;

end;

end;

dom p c= dom s by A3, PARTFUN1:def 4;
hence p c= s1 +* (DataPart s2) by A5, GRFUNC_1:8; :: thesis: verum