let p be preProgram of SCM+FSA; :: thesis: for k being Nat holds UsedILoc p = UsedILoc (Shift (p,k))
let k be Nat; :: thesis: UsedILoc p = UsedILoc (Shift (p,k))
dom p c= NAT ;
then rng p = rng (Shift (p,k)) by VALUED_1:26;
hence UsedILoc p = UsedILoc (Shift (p,k)) ; :: thesis: verum