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