consider X being non empty set such that
A1: the Instructions of S c= [:NAT,(NAT *),(X *):] by Def17;
I in the Instructions of S ;
then AddressPart I in X * by A1, RECDEF_2:2;
hence ( AddressPart I is Function-like & AddressPart I is Relation-like ) ; :: thesis: verum