let l be Instruction-Location of SCMPDS ; :: thesis: l = locnum l
thus locnum l = il. (locnum l)
.= l by Def1 ; :: thesis: verum