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