let I be preProgram of SCM+FSA; :: thesis: for x being set
for k being Element of NAT st x in dom (ProgramPart (Relocated (I,k))) holds
(ProgramPart (Relocated (I,k))) . x = (Relocated (I,k)) . x
let x be set ; :: thesis: for k being Element of NAT st x in dom (ProgramPart (Relocated (I,k))) holds
(ProgramPart (Relocated (I,k))) . x = (Relocated (I,k)) . x
let k be Element of NAT ; :: thesis: ( x in dom (ProgramPart (Relocated (I,k))) implies (ProgramPart (Relocated (I,k))) . x = (Relocated (I,k)) . x )
A1: ProgramPart (Relocated (I,k)) c= Relocated (I,k) by RELAT_1:88;
assume x in dom (ProgramPart (Relocated (I,k))) ; :: thesis: (ProgramPart (Relocated (I,k))) . x = (Relocated (I,k)) . x
hence (ProgramPart (Relocated (I,k))) . x = (Relocated (I,k)) . x by A1, GRFUNC_1:8; :: thesis: verum