let I be preProgram of SCM+FSA; :: thesis: for k being Element of NAT holds Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))
let k be Element of NAT ; :: thesis: Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))
A1: dom (Reloc (I,k)) = { (m + k) where m is Nat : m in dom I } by COMPOS_1:33;
A2: dom (Directed I) = dom I by FUNCT_4:99;
A3: dom (Reloc ((Directed I),k)) = { (m + k) where m is Nat : m in dom I } by A2, COMPOS_1:33;

A4: now :: thesis: for x being object st x in { (m + k) where m is Nat : m in dom I } holds
(Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x

let x be object ; :: thesis: ( x in { (m + k) where m is Nat : m in dom I } implies (Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x )
assume A5: x in { (m + k) where m is Nat : m in dom I } ; :: thesis: (Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x
then consider n being Nat such that
A6: x = n + k and
A7: n in dom I ;
dom (Directed I) = dom I by FUNCT_4:99;
then reconsider i = (Directed I) . n as Instruction of SCM+FSA by A7, FUNCT_1:106;
reconsider i0 = I . n as Instruction of SCM+FSA by A7, FUNCT_1:106;

A8: now :: thesis: ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = IncAddr (i,k)

per cases ( i0 = halt SCM+FSA or i0 <> halt SCM+FSA ) ;

suppose A9: i0 = halt SCM+FSA ; :: thesis: ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = IncAddr (i,k)

then A10: i = goto (card I) by A7, FUNCT_4:106;
A11: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:35
.= halt SCM+FSA by A9, COMPOS_0:4 ;
then (Reloc (I,k)) . x in {(halt SCM+FSA)} by TARSKI:def 1;
then (Reloc (I,k)) . x in dom ((halt SCM+FSA) .--> (goto ((card I) + k))) ;
then x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by A1, A5, FUNCT_1:11;
hence ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) . x by FUNCT_4:13
.= ((halt SCM+FSA) .--> (goto ((card I) + k))) . ((Reloc (I,k)) . x) by A1, A5, FUNCT_1:13
.= goto ((card I) + k) by A11, FUNCOP_1:72
.= IncAddr (i,k) by A10, SCMFSA_4:1 ;
:: thesis: verum

end;

suppose A12: i0 <> halt SCM+FSA ; :: thesis: ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = IncAddr (i,k)

A13: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:35;
A14: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
InsCode i0 <> 0 by A12, SCMFSA_2:95;
then IncAddr (i0,k) <> halt SCM+FSA by A14, COMPOS_0:def 9;
then not (Reloc (I,k)) . x in {(halt SCM+FSA)} by A13, TARSKI:def 1;
then not (Reloc (I,k)) . x in dom ((halt SCM+FSA) .--> (goto ((card I) + k))) ;
then not x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by FUNCT_1:11;
hence ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = (Reloc (I,k)) . x by FUNCT_4:11
.= IncAddr (i,k) by A12, A13, FUNCT_4:105 ;
:: thesis: verum

end;

end;

end;

thus (Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x by A8, A2, A6, A7, COMPOS_1:35; :: thesis: verum

end;

dom ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) = { (m + k) where m is Nat : m in dom I } by A1, FUNCT_4:99;
hence Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k))) by A3, A4, FUNCT_1:2; :: thesis: verum