f . d is Element of NAT ;
hence f . d is Instruction-Location of S by Def4; :: thesis: verum