let I, J be Program of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA st l in dom I & I . l <> halt SCM+FSA holds
(I ';' J) . l = I . l
let l be Instruction-Location of SCM+FSA ; :: thesis: ( l in dom I & I . l <> halt SCM+FSA implies (I ';' J) . l = I . l )
assume that
A1: l in dom I and
A2: I . l <> halt SCM+FSA ; :: thesis: (I ';' J) . l = I . l
ProgramPart (Relocated J,(card I)) = IncAddr [(Shift (ProgramPart J),(card I))],(card I) by SCMFSA_5:2;
then A3: dom (ProgramPart (Relocated J,(card I))) = dom (Shift (ProgramPart J),(card I)) by SCMFSA_4:def 6;

A4: now

assume l in dom (ProgramPart (Relocated J,(card I))) ; :: thesis: contradiction
then l in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart J) } by A3, VALUED_1:def 12;
then consider m being Element of NAT such that
A5: l = m + (card I) and
m in dom (ProgramPart J) ;
m + (card I) < card I by A1, A5, Th15;
hence contradiction by NAT_1:11; :: thesis: verum

end;

thus (I ';' J) . l = (Directed I) . l by A4, FUNCT_4:12
.= I . l by A2, FUNCT_4:111 ; :: thesis: verum