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

A4: now

let x be set ; :: thesis: ( x in { (m + k) where m is Element of NAT : m in dom I } implies (Reloc ((Directed I),k)) . x = (Directed ((Reloc (I,k)),((card I) + k))) . x )
assume A5: x in { (m + k) where m is Element of NAT : m in dom I } ; :: thesis: (Reloc ((Directed I),k)) . x = (Directed ((Reloc (I,k)),((card I) + k))) . x
then consider n being Element of NAT such that
A6: x = n + k and
A7: n in dom I ;
dom (Directed I) = dom I by FUNCT_4:105;
then reconsider i = (Directed I) . n as Instruction of SCM+FSA by A7, FUNCT_1:176;
reconsider i0 = I . n as Instruction of SCM+FSA by A7, FUNCT_1:176;

A8: now

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

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

then A10: i = goto (card I) by A7, FUNCT_4:112;
A11: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:122
.= halt SCM+FSA by A9, COMPOS_1:93 ;
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))) by FUNCOP_1:19;
then x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by A1, A5, FUNCT_1:21;
hence (Directed ((Reloc (I,k)),((card I) + k))) . x = (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) . x by FUNCT_4:14
.= ((halt SCM+FSA) .--> (goto ((card I) + k))) . ((Reloc (I,k)) . x) by A1, A5, FUNCT_1:23
.= goto ((card I) + k) by A11, FUNCOP_1:87
.= IncAddr (i,k) by A10, SCMFSA_4:14 ;
:: thesis: verum

end;

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

A13: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:122;
InsCode i0 <> 0 by A12, SCMFSA_2:122;
then IncAddr (i0,k) <> halt SCM+FSA by COMPOS_1:def 38, SCMFSA_2:124;
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))) by FUNCOP_1:19;
then not x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by FUNCT_1:21;
hence (Directed ((Reloc (I,k)),((card I) + k))) . x = (Reloc (I,k)) . x by FUNCT_4:12
.= IncAddr (i,k) by A12, A13, FUNCT_4:111 ;
:: thesis: verum

end;

end;

end;

thus (Reloc ((Directed I),k)) . x = (Directed ((Reloc (I,k)),((card I) + k))) . x by A8, A2, A6, A7, COMPOS_1:122; :: thesis: verum

end;

dom (Directed ((Reloc (I,k)),((card I) + k))) = { (m + k) where m is Element of NAT : m in dom I } by A1, FUNCT_4:105;
hence Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k)) by A3, A4, FUNCT_1:9; :: thesis: verum