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 A1: ( p c= s1 & Relocated p,k c= s2 ) ; :: thesis: p c= s1 +* (DataPart s2)
reconsider s = s1 +* (s2 | (Int-Locations \/ FinSeq-Locations )) as State of SCM+FSA ;
set s3 = DataPart s2;
A2: dom p c= ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by AMI_1:80, SCMFSA_2:8;
then A3: dom p c= dom s by AMI_1:79, SCMFSA_2:8;

now

let x be set ; :: thesis: ( x in dom p implies p . b₁ = s . b₁ )
assume A4: x in dom p ; :: thesis: p . b₁ = s . b₁
( Int-Locations c= dom s2 & FinSeq-Locations c= dom s2 ) by SCMFSA_2:69, SCMFSA_2:70;
then Int-Locations \/ FinSeq-Locations = (dom s2) /\ (Int-Locations \/ FinSeq-Locations ) by XBOOLE_1:8, XBOOLE_1:28;
then A5: dom (DataPart s2) = Int-Locations \/ FinSeq-Locations by RELAT_1:90, SCMFSA_2:127;
A6: ( x in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} or x in NAT ) by A2, A4, XBOOLE_0:def 3;

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

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

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

end;

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

set DPp = DataPart p;
x in (dom p) /\ (Int-Locations \/ FinSeq-Locations ) by A4, A8, XBOOLE_0:def 4;
then A10: x in dom (DataPart p) by RELAT_1:90, SCMFSA_2:127;
DataPart p c= p by RELAT_1:88;
then A11: (DataPart p) . x = p . x by A10, GRFUNC_1:8;
DataPart p = DataPart (Relocated p,k) by Th1;
then DataPart p c= Relocated p,k by RELAT_1:88;
then A12: DataPart p c= s2 by A1, XBOOLE_1:1;
then A13: (DataPart p) . x = s2 . x by A10, GRFUNC_1:8;
A14: dom (DataPart p) c= dom s2 by A12, GRFUNC_1:8;
A15: s2 . x = (DataPart s2) . x by A8, FUNCT_1:72, SCMFSA_2:127;
x in (dom s2) /\ (Int-Locations \/ FinSeq-Locations ) by A8, A10, A14, XBOOLE_0:def 4;
then x in dom (DataPart s2) by RELAT_1:90, SCMFSA_2:127;
hence p . x = s . x by A11, A13, A15, FUNCT_4:14, SCMFSA_2:127; :: thesis: verum

end;

suppose A16: 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 A16, 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, A4, GRFUNC_1:8; :: thesis: verum

end;

end;

end;

hence p c= s1 +* (DataPart s2) by A3, GRFUNC_1:8, SCMFSA_2:127; :: thesis: verum