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 COMPOS_1:140;
hence I c= I +* (Start-At (l,SCM+FSA)) by FUNCT_4:33; :: thesis: verum