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