let s be State of ; :: thesis: for loc being Instruction-Location of SCMPDS holds (s +* (Start-At loc)) . (IC SCMPDS ) = loc
let loc be Instruction-Location of SCMPDS ; :: thesis: (s +* (Start-At loc)) . (IC SCMPDS ) = loc
thus (s +* (Start-At loc)) . (IC SCMPDS ) = IC (s +* (Start-At loc))
.= loc by AMI_1:111 ; :: thesis: verum