let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS st IC s = 0 holds
s +* (Initialized I) = s +* I
let I be Program of SCMPDS ; :: thesis: ( IC s = 0 implies s +* (Initialized I) = s +* I )
set SA0 = Start-At 0 ,SCMPDS ;
A1: dom I misses dom (Start-At 0 ,SCMPDS ) by SCMPDS_4:54;
assume IC s = 0 ; :: thesis: s +* (Initialized I) = s +* I
then Initialized s = s by Th4;
hence s +* I = (s +* (Start-At 0 ,SCMPDS )) +* I by SCMPDS_5:def 4
.= s +* ((Start-At 0 ,SCMPDS ) +* I) by FUNCT_4:15
.= s +* (Initialized I) by A1, FUNCT_4:36 ;
:: thesis: verum