let s be State of SCMPDS ; :: thesis: for loc being Element of NAT
for I being Program of SCMPDS st loc in dom I holds
(s +* (Initialized I)) . loc = I . loc
let loc be Element of NAT ; :: thesis: for I being Program of SCMPDS st loc in dom I holds
(s +* (Initialized I)) . loc = I . loc
let I be Program of SCMPDS ; :: thesis: ( loc in dom I implies (s +* (Initialized I)) . loc = I . loc )
assume A1: loc in dom I ; :: thesis: (s +* (Initialized I)) . loc = I . loc
set II = Initialized I;
A2: I c= Initialized I by SCMPDS_4:9;
then dom I c= dom (Initialized I) by GRFUNC_1:8;
hence (s +* (Initialized I)) . loc = (Initialized I) . loc by A1, FUNCT_4:14
.= I . loc by A1, A2, GRFUNC_1:8 ;
:: thesis: verum