consider X being non empty set such that
A1: the Instructions of S c= [:NAT ,(X * ):] by AMI_1:def 32;
I in the Instructions of S ;
then AddressPart I in X * by A1, MCART_1:10;
hence AddressPart I is FinSequence ; :: thesis: verum