let I, J be Program of ; :: 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
A3: dom (Reloc (J,(card I))) = dom (Shift (J,(card I))) by COMPOS_1:def 19;

now

assume l in dom (Reloc (J,(card I))) ; :: thesis: contradiction
then l in { (m + (card I)) where m is Element of NAT : m in dom 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 J ;
m + (card I) < card I by A1, A4, AFINSQ_1:66;
hence contradiction by NAT_1:11; :: thesis: verum

end;

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