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