let s be State of SCM+FSA ; :: thesis: for P being FinPartState of SCM+FSA
for l being Element of NAT holds IC (s +* (P +* (Start-At l,SCM+FSA ))) = l
let I be FinPartState of SCM+FSA ; :: thesis: for l being Element of NAT holds IC (s +* (I +* (Start-At l,SCM+FSA ))) = l
let l be Element of NAT ; :: thesis: IC (s +* (I +* (Start-At l,SCM+FSA ))) = l
thus IC (s +* (I +* (Start-At l,SCM+FSA ))) = IC ((s +* I) +* (Start-At l,SCM+FSA )) by FUNCT_4:15
.= l by FUNCT_4:121 ; :: thesis: verum