let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis: for P being preProgram of S holds Reloc (P,0) = P
let P be preProgram of S; :: thesis: Reloc (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:1;

now

let x be set ; :: thesis: ( ( x in dom (Reloc (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 (Reloc (P,0)) ) )
A3: dom (Reloc (P,0)) = { (m + 0) where m is Element of NAT : m in dom P } by Th117;

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

assume x in dom (Reloc (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 A3;
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 (Reloc (P,0))
then consider m being Element of NAT such that
A4: x = m and
A5: m in dom P ;
x = m + 0 by A4;
hence x in dom (Reloc (P,0)) by A3, A5; :: thesis: verum

end;

then A6: dom (Reloc (P,0)) = { m where m is Element of NAT : m in dom P } by TARSKI:1;

now

let x be set ; :: thesis: ( x in { m where m is Element of NAT : m in dom P } implies (Reloc (P,0)) . x = P . x )
assume x in { m where m is Element of NAT : m in dom P } ; :: thesis: (Reloc (P,0)) . x = P . x
then consider n being Element of NAT such that
A7: x = n and
A8: n in dom P ;
dom (Shift (P,0)) = { (m + 0) where m is Element of NAT : m in dom P } by VALUED_1:def 12;
then A10: n + 0 in dom (Shift (P,0)) by A8;
then A11: (Shift (P,0)) /. (n + 0) = (Shift (P,0)) . (n + 0) by PARTFUN1:def 6
.= P . n by A8, VALUED_1:def 12 ;
then consider i being Instruction of S such that
A12: i = P . n ;
thus (Reloc (P,0)) . x = IncAddr (i,0) by A10, A11, A12, A7, Def40
.= P . x by A7, A12, Th91 ; :: thesis: verum

end;

hence Reloc (P,0) = P by A2, A6, FUNCT_1:2; :: thesis: verum