let I be Program of ; :: thesis: for l being Instruction-Location of SCMPDS holds I c= I +* (Start-At l)
let l be Instruction-Location of SCMPDS ; :: thesis: I c= I +* (Start-At l)
reconsider n = l as Element of NAT by ORDINAL1:def 13;
l = inspos n ;
then dom I misses dom (Start-At l) by SCMPDS_4:54;
hence I c= I +* (Start-At l) by FUNCT_4:33; :: thesis: verum