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 = (stop I) . loc
.= I . loc by A1, Th19 ; :: thesis: verum