let s be data-only FinPartState of SCM+FSA ; :: thesis: for p being FinPartState of SCM+FSA
for k being Element of NAT st IC SCM+FSA in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s
let p be FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT st IC SCM+FSA in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s
let k be Element of NAT ; :: thesis: ( IC SCM+FSA in dom p implies Relocated (p +* s),k = (Relocated p,k) +* s )
A1: dom s c= Int-Locations \/ FinSeq-Locations by AMI_1:139, SCMFSA_2:127;
then dom s misses NAT by Lm1, XBOOLE_1:63;
then A2: ProgramPart (p +* s) = ProgramPart p by FUNCT_4:76;
not IC SCM+FSA in Int-Locations \/ FinSeq-Locations

proof

assume A3: IC SCM+FSA in Int-Locations \/ FinSeq-Locations ; :: thesis: contradiction

per cases ( IC SCM+FSA in Int-Locations or IC SCM+FSA in FinSeq-Locations ) by A3, XBOOLE_0:def 3;

suppose IC SCM+FSA in Int-Locations ; :: thesis: contradiction

then IC SCM+FSA is Int-Location by SCMFSA_2:11;
hence contradiction by SCMFSA_2:81; :: thesis: verum

end;

suppose IC SCM+FSA in FinSeq-Locations ; :: thesis: contradiction

then IC SCM+FSA is FinSeq-Location by SCMFSA_2:12;
hence contradiction by SCMFSA_2:82; :: thesis: verum

end;

end;

end;

then A4: not IC SCM+FSA in dom s by A1;
assume IC SCM+FSA in dom p ; :: thesis: Relocated (p +* s),k = (Relocated p,k) +* s
then A6: IC SCM+FSA in (dom p) \/ (dom s) by XBOOLE_0:def 3;
A7: IC (p +* s) = (p +* s) . (IC SCM+FSA )
.= IC p by A6, A4, FUNCT_4:def 1 ;
DataPart (p +* s) = (DataPart p) +* (DataPart s) by FUNCT_4:75
.= (DataPart p) +* s by A1, RELAT_1:97, SCMFSA_2:127 ;
hence Relocated (p +* s),k = (Relocated p,k) +* s by A7, A2, FUNCT_4:15; :: thesis: verum