let I, J be Program of ; :: thesis: for i being Instruction of SCM+FSA holds ((I ";" i) ";" J) . ((card I) + 1) = goto ((card I) + 2)
let i be Instruction of SCM+FSA; :: thesis: ((I ";" i) ";" J) . ((card I) + 1) = goto ((card I) + 2)
set x1 = card I;
A1: card (I ";" i) = (card I) + 2 by SCMFSA6A:34;
A2: card (Macro i) = 2 by COMPOS_1:56;
set x2 = (card I) + 1;
(card I) + 1 < (card I) + 2 by XREAL_1:6;
then A3: (card I) + 1 in dom (I ";" i) by A1, AFINSQ_1:66;
(Macro i) . 1 = halt SCM+FSA by COMPOS_1:59;
then (I ";" (Macro i)) . ((card I) + 1) = IncAddr ((halt SCM+FSA),(card I)) by A2, Th16;
then A4: (I ";" i) . ((card I) + 1) = IncAddr ((halt SCM+FSA),(card I)) by SCMFSA6A:def 6
.= halt SCM+FSA by COMPOS_0:4 ;
thus ((I ";" i) ";" J) . ((card I) + 1) = (Directed (I ";" i)) . ((card I) + 1) by A3, SCMFSA8A:14
.= goto ((card I) + 2) by A1, A3, A4, SCMFSA8A:16 ; :: thesis: verum