A1: the Instructions of S c= [:NAT ,(((union N) \/ the carrier of S) * ):] by AMI_1:def 32;
I in the Instructions of S ;
then AddressPart I in ((union N) \/ the carrier of S) * by A1, MCART_1:10;
hence AddressPart I is FinSequence of (union N) \/ the carrier of S by FINSEQ_1:def 11; :: thesis: verum