let s be State of ; :: thesis: for l1, l2 being Instruction-Location of SCMPDS holds (s +* (Start-At l1)) +* (Start-At l2) = s +* (Start-At l2)
let l1, l2 be Instruction-Location of SCMPDS ; :: thesis: (s +* (Start-At l1)) +* (Start-At l2) = s +* (Start-At l2)
A1: dom (Start-At l1) = {(IC SCMPDS )} by FUNCOP_1:19
.= dom (Start-At l2) by FUNCOP_1:19 ;
thus (s +* (Start-At l1)) +* (Start-At l2) = s +* ((Start-At l1) +* (Start-At l2)) by FUNCT_4:15
.= s +* (Start-At l2) by A1, FUNCT_4:20 ; :: thesis: verum