let I be Program of SCMPDS ; :: 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;
A1: l = inspos n ;
dom I misses dom (Start-At l) by A1, SCMPDS_4:54;
hence I c= I +* (Start-At l) by FUNCT_4:33; :: thesis: verum