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