let loc be Instruction-Location of SCMPDS ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
loc in dom (stop I)
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies loc in dom (stop I) )
assume A1: loc in dom I ; :: thesis: loc in dom (stop I)
dom I c= dom (I ';' (Stop SCMPDS )) by SCMPDS_4:39;
then dom I c= dom (stop I) by SCMPDS_4:def 7;
hence loc in dom (stop I) by A1; :: thesis: verum