let I be Program of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA holds I c= I +* (Start-At l)
let l be Instruction-Location of SCM+FSA ; :: thesis: I c= I +* (Start-At l)
reconsider n = l as Element of NAT by ORDINAL1:def 13;
A1: l = insloc n ;
dom I misses dom (Start-At l) by A1, SF_MASTR:64;
hence I c= I +* (Start-At l) by FUNCT_4:33; :: thesis: verum