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;
A2: l = insloc n ;
thus x in { m where m is Element of NAT : m in dom P } by A1, A2; :: thesis: verum

end;

assume x in { m where m is Element of NAT : m in dom P } ; :: thesis: x in dom P
then consider m being Element of NAT such that
A3: ( x = m & m in dom P ) ;
thus x in dom P by A3; :: thesis: verum

end;

then A4: dom P = { m where m is Element of NAT : m in dom P } by TARSKI:2;
A5: 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 )) ) )
A6: dom (ProgramPart (Relocated P,0 )) = { (m + 0 ) where m is Element of NAT : m in dom P } by A5, 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 consider n being Element of NAT such that
A7: ( x = n + 0 & n in dom P ) by A6;
thus x in { m where m is Element of NAT : m in dom P } by A7; :: 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
A8: ( x = m & m in dom P ) ;
( x = insloc (m + 0 ) & insloc m in dom P ) by A8;
hence x in dom (ProgramPart (Relocated P,0 )) by A6; :: thesis: verum

end;

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

end;

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