consider X being non empty set such that
A1: S c= [:NAT,(NAT *),(X *):] by Def1;
I in S ;
then AddressPart I in X * by A1, RECDEF_2:2;
hence for b₁ being Function st b₁ = AddressPart I holds
b₁ is FinSequence-like ; :: thesis: verum