reconsider x = x as Element of dom T by A1;
T . x is Element of NAT ;
hence T . x is Instruction-Location of S by Def4; :: thesis: verum