let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for s being State of S
for l1, l2 being Element of NAT holds (s +* (Start-At l1,S)) +* (Start-At l2,S) = s +* (Start-At l2,S)
let S be non empty IC-Ins-separated AMI-Struct of N; :: thesis: for s being State of S
for l1, l2 being Element of NAT holds (s +* (Start-At l1,S)) +* (Start-At l2,S) = s +* (Start-At l2,S)
let s be State of S; :: thesis: for l1, l2 being Element of NAT holds (s +* (Start-At l1,S)) +* (Start-At l2,S) = s +* (Start-At l2,S)
let l1, l2 be Element of NAT ; :: thesis: (s +* (Start-At l1,S)) +* (Start-At l2,S) = s +* (Start-At l2,S)
A1: dom (Start-At l1,S) = {(IC S)} by FUNCOP_1:19
.= dom (Start-At l2,S) by FUNCOP_1:19 ;
thus (s +* (Start-At l1,S)) +* (Start-At l2,S) = s +* ((Start-At l1,S) +* (Start-At l2,S)) by FUNCT_4:15
.= s +* (Start-At l2,S) by A1, FUNCT_4:20 ; :: thesis: verum