set SA0 = Start-At 0 ,SCMPDS ;
let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds (Initialize s) +* I = s +* (Initialize I)
let I be Program of SCMPDS ; :: thesis: (Initialize s) +* I = s +* (Initialize I)
A2: not IC SCMPDS in dom I by COMPOS_1:3;
dom (Start-At 0 ,SCMPDS ) = {(IC SCMPDS )} by FUNCOP_1:19;
then A1: dom I misses dom (Start-At 0 ,SCMPDS ) by A2, ZFMISC_1:56;
thus (Initialize s) +* I = (s +* (Start-At 0 ,SCMPDS )) +* I
.= s +* ((Start-At 0 ,SCMPDS ) +* I) by FUNCT_4:15
.= s +* (I +* (Start-At 0 ,SCMPDS )) by A1, FUNCT_4:36
.= s +* (Initialize I) ; :: thesis: verum