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 Instruction-Location of SCM+FSA by A1, AMI_1:def 4;
reconsider n = l as Element of NAT by ORDINAL1:def 13;
l = insloc 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 AMI_1:105;

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 )) = { (m + 0 ) where m is Element of NAT : m in dom P } by A3, SCMFSA_5:3;

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 = insloc (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: insloc n in dom (ProgramPart P) by A9, AMI_1:105;
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: insloc (n + 0 ) in dom (Shift (ProgramPart P),0 ) by A3, A9;
then A12: pi [(Shift (ProgramPart P),0 )],(n + 0 ) = (Shift (ProgramPart P),0 ) . (insloc (n + 0 )) by AMI_1:def 47
.= (ProgramPart P) . (insloc n) by A10, VALUED_1:def 12
.= P . (insloc n) by AMI_1:105 ;
then consider i being Instruction of SCM+FSA such that
A13: i = P . (insloc n) ;
thus (ProgramPart (Relocated P,0 )) . x = (IncAddr [(Shift (ProgramPart P),0 )],0 ) . (insloc (n + 0 )) by A8, SCMFSA_5:2
.= IncAddr i,0 by A11, A12, A13, SCMFSA_4:def 6
.= P . x by A8, A13, Th8 ; :: thesis: verum

end;

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