let loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
(Initialize (stop I)) . loc = I . loc
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies (Initialize (stop I)) . loc = I . loc )
assume A1: loc in dom I ; :: thesis: (Initialize (stop I)) . loc = I . loc
then loc in dom (stop I) by Th18;
hence (Initialize (stop I)) . loc = (stop I) . loc by SCMPDS_4:33
.= I . loc by A1, Th19 ;
:: thesis: verum