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