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

( b_{1} is Function-like & b_{1} is Relation-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