let c be Element of the Instructions of SCM+FSA; :: thesis:
reconsider d = c as Instruction of SCM+FSA ;
thus UIL . c = UsedIntLoc d by A1
.= UIL2 . c by A3 ; :: thesis:

end;

then A5: UIL = UIL2 by FUNCT_2:113;
A6: dom (Shift (p,k)) = { (m + k) where m is Element of NAT : m in dom p } by VALUED_1:def 12;

let y be set ; :: thesis:

assume y in rng (Shift (p,k)) ; :: thesis:
then consider x being set such that
A7: x in dom (Shift (p,k)) and
A8: y = (Shift (p,k)) . x by FUNCT_1:def 5;
consider m being Element of NAT such that
A9: x = m + k and
A10: m in dom p by A6, A7;
(Shift (p,k)) . x = p . m by A9, A10, VALUED_1:def 12;
hence y in rng p by A8, A10, FUNCT_1:def 5; :: thesis:

end;

assume y in rng p ; :: thesis:
then consider x being set such that
A11: x in dom p and
A12: y = p . x by FUNCT_1:def 5;
dom p c= NAT by RELAT_1:def 18;
then reconsider x9 = x as Element of NAT by A11;
reconsider m = x9 as Element of NAT ;
( m + k in dom (Shift (p,k)) & (Shift (p,k)) . (m + k) = p . m ) by A6, A11, VALUED_1:def 12;
hence y in rng (Shift (p,k)) by A12, FUNCT_1:def 5; :: thesis:

end;