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