let I, J be Program of SCM+FSA ; :: thesis: for l being Element of NAT st l in dom I & I . l <> halt SCM+FSA holds
(I ';' J) . l = I . l
let l be Element of NAT ; :: 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)) = Reloc (ProgramPart J),(card I) by AMISTD_2:69;
then A3: dom (ProgramPart (Relocated J,(card I))) = dom (Shift (ProgramPart J),(card I)) by AMISTD_2:def 15;

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
A4: l = m + (card I) and
m in dom (ProgramPart J) ;
m + (card I) < card I by A1, A4, AFINSQ_1:70;
hence contradiction by NAT_1:11; :: thesis: verum

end;

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