let P be preProgram of SCM+FSA; :: thesis: ProgramPart (Relocated (P,0)) = P

now

let x be set ; :: thesis: ( ( x in dom P implies x in { m where m is Element of NAT : m in dom P } ) & ( x in { m where m is Element of NAT : m in dom P } implies x in dom P ) )

hereby :: thesis: ( x in { m where m is Element of NAT : m in dom P } implies x in dom P )

assume A1: x in dom P ; :: thesis: x in { m where m is Element of NAT : m in dom P }
dom P c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A1;
reconsider n = l as Element of NAT ;
l = n ;
hence x in { m where m is Element of NAT : m in dom P } by A1; :: thesis: verum

end;

assume x in { m where m is Element of NAT : m in dom P } ; :: thesis: x in dom P
then ex m being Element of NAT st
( x = m & m in dom P ) ;
hence x in dom P ; :: thesis: verum

end;

then A2: dom P = { m where m is Element of NAT : m in dom P } by TARSKI:2;
A3: dom (ProgramPart P) = dom P by RELAT_1:209;

now

let x be set ; :: thesis: ( ( x in dom (ProgramPart (Relocated (P,0))) implies x in { m where m is Element of NAT : m in dom P } ) & ( x in { m where m is Element of NAT : m in dom P } implies x in dom (ProgramPart (Relocated (P,0))) ) )
A4: dom (ProgramPart (Relocated (P,0))) = dom (Reloc ((ProgramPart P),0)) by COMPOS_1:116
.= { (m + 0) where m is Element of NAT : m in dom P } by A3, COMPOS_1:117 ;

hereby :: thesis: ( x in { m where m is Element of NAT : m in dom P } implies x in dom (ProgramPart (Relocated (P,0))) )

assume x in dom (ProgramPart (Relocated (P,0))) ; :: thesis: x in { m where m is Element of NAT : m in dom P }
then ex n being Element of NAT st
( x = n + 0 & n in dom P ) by A4;
hence x in { m where m is Element of NAT : m in dom P } ; :: thesis: verum

end;

assume x in { m where m is Element of NAT : m in dom P } ; :: thesis: x in dom (ProgramPart (Relocated (P,0)))
then consider m being Element of NAT such that
A5: x = m and
A6: m in dom P ;
x = m + 0 by A5;
hence x in dom (ProgramPart (Relocated (P,0))) by A4, A6; :: thesis: verum

end;

then A7: dom (ProgramPart (Relocated (P,0))) = { m where m is Element of NAT : m in dom P } by TARSKI:2;

now

let x be set ; :: thesis: ( x in { m where m is Element of NAT : m in dom P } implies (ProgramPart (Relocated (P,0))) . x = P . x )
assume x in { m where m is Element of NAT : m in dom P } ; :: thesis: (ProgramPart (Relocated (P,0))) . x = P . x
then consider n being Element of NAT such that
A8: x = n and
A9: n in dom P ;
A10: n in dom (ProgramPart P) by A9, RELAT_1:209;
dom (Shift ((ProgramPart P),0)) = { (m + 0) where m is Element of NAT : m in dom (ProgramPart P) } by VALUED_1:def 12;
then A11: n + 0 in dom (Shift ((ProgramPart P),0)) by A3, A9;
then A12: (Shift ((ProgramPart P),0)) /. (n + 0) = (Shift ((ProgramPart P),0)) . (n + 0) by PARTFUN1:def 8
.= (ProgramPart P) . n by A10, VALUED_1:def 12
.= P . n by RELAT_1:209 ;
then consider i being Instruction of SCM+FSA such that
A13: i = P . n ;
thus (ProgramPart (Relocated (P,0))) . x = (Reloc ((ProgramPart P),0)) . (n + 0) by A8, COMPOS_1:116
.= IncAddr (i,0) by A11, A12, A13, COMPOS_1:def 40
.= P . x by A8, A13, COMPOS_1:91 ; :: thesis: verum

end;

hence ProgramPart (Relocated (P,0)) = P by A2, A7, FUNCT_1:9; :: thesis: verum