let I, J be Program of ; :: thesis: for l being Nat st l in dom I & I . l <> halt SCM+FSA holds
(I ";" J) . l = I . l
let l be 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
Reloc (J,(card I)) = IncAddr ((Shift (J,(card I))),(card I)) by COMPOS_1:34;
then A3: dom (Reloc (J,(card I))) = dom (Shift (J,(card I))) by COMPOS_1:def 21;
A4: (card (stop I)) -' 1 = card I by COMPOS_1:71;
A5: card (stop (Directed I)) = card (stop I) by Lm2;

now :: thesis: not l in dom (Reloc (J,(card I)))

assume l in dom (Reloc (J,(card I))) ; :: thesis: contradiction
then l in { (m + (card I)) where m is Nat : m in dom J } by A3, VALUED_1:def 12;
then consider m being Nat such that
A6: l = m + (card I) and
m in dom J ;
m + (card I) < card I by A1, A6, AFINSQ_1:66;
hence contradiction by NAT_1:11; :: thesis: verum

end;

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