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