let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
let p be autonomic FinPartState of SCM+FSA ; :: thesis: for s1, s2 being State of SCM+FSA st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of SCM+FSA ; :: 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 +* (s2 | (Int-Locations \/ FinSeq-Locations )) as State of SCM+FSA ;
A3: dom p c= ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by RELAT_1:def 18, SCMFSA_2:8;

A4: now

A5: FinSeq-Locations c= dom s2 by SCMFSA_2:70;
Int-Locations c= dom s2 by SCMFSA_2:69;
then Int-Locations \/ FinSeq-Locations = (dom s2) /\ (Int-Locations \/ FinSeq-Locations ) by A5, XBOOLE_1:8, XBOOLE_1:28;
then A6: dom (DataPart s2) = Int-Locations \/ FinSeq-Locations by RELAT_1:90, SCMFSA_2:127;
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 (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} or x in NAT ) by A3, A7, XBOOLE_0:def 3;

per cases ( x in {(IC SCM+FSA )} or x in Int-Locations \/ FinSeq-Locations or x in NAT ) by A8, XBOOLE_0:def 3;

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

A10: not IC SCM+FSA in Int-Locations \/ FinSeq-Locations by SCMFSA_3:1, SCMFSA_3:2, XBOOLE_0:def 3;
x = IC SCM+FSA by A9, TARSKI:def 1;
then s1 . x = s . x by A6, A10, FUNCT_4:12, SCMFSA_2:127;
hence p . x = s . x by A1, A7, GRFUNC_1:8; :: thesis: verum

end;

suppose A11: x in Int-Locations \/ FinSeq-Locations ; :: thesis: p . b₁ = s . b₁

set DPp = DataPart p;
x in (dom p) /\ (Int-Locations \/ FinSeq-Locations ) by A7, A11, XBOOLE_0:def 4;
then A12: x in dom (DataPart p) by RELAT_1:90, SCMFSA_2:127;
DataPart p = DataPart (Relocated p,k) by Th1;
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) /\ (Int-Locations \/ FinSeq-Locations ) by A11, A12, XBOOLE_0:def 4;
then A14: x in dom (DataPart s2) by RELAT_1:90, SCMFSA_2:127;
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, SCMFSA_2:127;
(DataPart p) . x = s2 . x by A12, A13, GRFUNC_1:8;
hence p . x = s . x by A15, A16, A14, FUNCT_4:14, SCMFSA_2:127; :: thesis: verum

end;

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

now

assume x in dom (DataPart s2) ; :: thesis: contradiction
then x in (dom s2) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90, SCMFSA_2:127;
then x in Int-Locations \/ FinSeq-Locations by XBOOLE_0:def 4;
hence contradiction by A17, Lm1, XBOOLE_0:3; :: thesis: verum

end;

then s1 . x = s . x by FUNCT_4:12, SCMFSA_2:127;
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, SCMFSA_2:8;
hence p c= s1 +* (DataPart s2) by A4, GRFUNC_1:8, SCMFSA_2:127; :: thesis: verum