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 COMPOS_1:116;
then A3: dom (ProgramPart (Relocated (J,(card I)))) = dom (Shift ((ProgramPart J),(card I))) by COMPOS_1:def 40;

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