let loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
(stop I) . loc = I . loc
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies (stop I) . loc = I . loc )
assume A1: loc in dom I ; :: thesis: (stop I) . loc = I . loc
thus (stop I) . loc = (I ';' (Stop SCMPDS )) . loc
.= I . loc by A1, SCMPDS_4:37 ; :: thesis: verum