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 )
assume A1: IC SCM+FSA in dom p ; :: thesis: Relocated (p +* s),k = (Relocated p,k) +* s
then A2: IC SCM+FSA in (dom p) \/ (dom s) by XBOOLE_0:def 3;
A3: not IC SCM+FSA in Int-Locations \/ FinSeq-Locations

proof

assume A4: 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 A4, 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;

A5: dom s c= Int-Locations \/ FinSeq-Locations by AMI_1:139, SCMFSA_2:127;
then A6: not IC SCM+FSA in dom s by A3;
IC SCM+FSA in dom (p +* s) by A2, FUNCT_4:def 1;
then A7: IC (p +* s) = (p +* s) . (IC SCM+FSA ) by AMI_1:def 43
.= p . (IC SCM+FSA ) by A2, A6, FUNCT_4:def 1
.= IC p by A1, AMI_1:def 43 ;
dom s misses NAT by A5, Lm1, XBOOLE_1:63;
then A8: ProgramPart (p +* s) = ProgramPart p by FUNCT_4:76;
A9: DataPart (p +* s) = (DataPart p) +* (DataPart s) by FUNCT_4:75
.= (DataPart p) +* s by A5, RELAT_1:97, SCMFSA_2:127 ;
thus Relocated (p +* s),k = (Relocated p,k) +* s by A7, A8, A9, FUNCT_4:15; :: thesis: verum