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_{1} being Function st b_{1} = AddressPart I holds

b_{1} is FinSequence-like
; :: thesis: verum

A1: S c= [:NAT,(NAT *),(X *):] by Def1;

I in S ;

then AddressPart I in X * by A1, RECDEF_2:2;

hence for b

b