let I be Program of SCMPDS ; :: thesis: for s being State of SCMPDS holds (s +* I) +* (Start-At 0 ,SCMPDS ) = (s +* (Start-At 0 ,SCMPDS )) +* I
let s be State of SCMPDS ; :: thesis: (s +* I) +* (Start-At 0 ,SCMPDS ) = (s +* (Start-At 0 ,SCMPDS )) +* I
A1: dom I misses dom (Start-At 0 ,SCMPDS ) by Th54;
then I +* (Start-At 0 ,SCMPDS ) = I \/ (Start-At 0 ,SCMPDS ) by FUNCT_4:32
.= (Start-At 0 ,SCMPDS ) +* I by A1, FUNCT_4:32 ;
hence (s +* I) +* (Start-At 0 ,SCMPDS ) = s +* ((Start-At 0 ,SCMPDS ) +* I) by FUNCT_4:15
.= (s +* (Start-At 0 ,SCMPDS )) +* I by FUNCT_4:15 ;
:: thesis: verum