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