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:33;
A2: dom (Directed I) = dom I by FUNCT_4:99;
A3: dom (Reloc ((Directed I),k)) = { (m + k) where m is Element of NAT : m in dom I } by A2, COMPOS_1:33;

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: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

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:106;
A11: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:35
.= halt SCM+FSA by A9, COMPOS_1:11 ;
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:13;
then x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by A1, A5, FUNCT_1:11;
hence (Directed ((Reloc (I,k)),((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: (Directed ((Reloc (I,k)),((card I) + k))) . x = IncAddr (i,k)

A13: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:35;
InsCode i0 <> 0 by A12, SCMFSA_2:95;
then IncAddr (i0,k) <> halt SCM+FSA by COMPOS_1:def 17, SCMFSA_2:97;
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:13;
then not x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by FUNCT_1:11;
hence (Directed ((Reloc (I,k)),((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 = (Directed ((Reloc (I,k)),((card I) + k))) . x by A8, A2, A6, A7, COMPOS_1:35; :: 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:99;
hence Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k)) by A3, A4, FUNCT_1:2; :: thesis: verum