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